DEFINITION pr0_gen_appl()
TYPE =
       ∀u1:T
         .∀t1:T
           .∀x:T
             .pr0 (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.pr0 u1 u2 λ:T.λt2:T.pr0 t1 t2
                    ex4_4
                      T
                      T
                      T
                      T
                      λy1:T.λz1:T.λ:T.λ:T.eq T t1 (THead (Bind Abst) y1 z1)
                      λ:T.λ:T.λu2:T.λt2:T.eq T x (THead (Bind Abbr) u2 t2)
                      λ:T.λ:T.λu2:T.λ:T.pr0 u1 u2
                      λ:T.λz1:T.λ:T.λt2:T.pr0 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.eq T t1 (THead (Bind b) y1 z1)
                      λb:B
                        .λ:T
                          .λ:T
                            .λu2:T
                              .λv2:T
                                .λt2:T
                                  .eq T x (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t2))
                      λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 u1 u2
                      λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
                      λ:B.λ:T.λz1:T.λ:T.λ:T.λt2:T.pr0 z1 t2)
BODY =
Show proof