DEFINITION pr3_gen_appl()
TYPE =
       ∀c:C
         .∀u1:T
           .∀t1:T
             .∀x:T
               .pr3 c (THead (Flat Appl) u1 t1) x
                 →(or3
                      ex3_2 T T λu2:T.λt2:T.eq T x (THead (Flat Appl) u2 t2) λu2:T.λ:T.pr3 c u1 u2 λ:T.λt2:T.pr3 c t1 t2
                      ex4_4
                        T
                        T
                        T
                        T
                        λ:T.λ:T.λu2:T.λt2:T.pr3 c (THead (Bind Abbr) u2 t2) x
                        λ:T.λ:T.λu2:T.λ:T.pr3 c u1 u2
                        λy1:T.λz1:T.λ:T.λ:T.pr3 c t1 (THead (Bind Abst) y1 z1)
                        λ:T.λz1:T.λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t2)
                      ex6_6
                        B
                        T
                        T
                        T
                        T
                        T
                        λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
                        λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c t1 (THead (Bind b) y1 z1)
                        λb:B
                          .λ:T
                            .λ:T
                              .λz2:T
                                .λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) x
                        λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c u1 u2
                        λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
                        λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2)
BODY =
Show proof