matita/matita/contribs/lambdadelta/basic_1/pr2/pr2.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "Basic-1/pr2/defs.ma".
  18
  19 include "Basic-1/pr0/pr0.ma".
  20
  21 include "Basic-1/getl/props.ma".
  22
  23 theorem pr2_confluence__pr2_free_free:
  24  \forall (c: C).(\forall (t0: T).(\forall (t1: T).(\forall (t2: T).((pr0 t0
  25 t1) \to ((pr0 t0 t2) \to (ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t:
  26 T).(pr2 c t2 t))))))))
  27 \def
  28  \lambda (c: C).(\lambda (t0: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda
  29 (H: (pr0 t0 t1)).(\lambda (H0: (pr0 t0 t2)).(ex2_ind T (\lambda (t: T).(pr0
  30 t2 t)) (\lambda (t: T).(pr0 t1 t)) (ex2 T (\lambda (t: T).(pr2 c t1 t))
  31 (\lambda (t: T).(pr2 c t2 t))) (\lambda (x: T).(\lambda (H1: (pr0 t2
  32 x)).(\lambda (H2: (pr0 t1 x)).(ex_intro2 T (\lambda (t: T).(pr2 c t1 t))
  33 (\lambda (t: T).(pr2 c t2 t)) x (pr2_free c t1 x H2) (pr2_free c t2 x H1)))))
  34 (pr0_confluence t0 t2 H0 t1 H))))))).
  35 (* COMMENTS
  36 Initial nodes: 135
  37 END *)
  38
  39 theorem pr2_confluence__pr2_free_delta:
  40  \forall (c: C).(\forall (d: C).(\forall (t0: T).(\forall (t1: T).(\forall
  41 (t2: T).(\forall (t4: T).(\forall (u: T).(\forall (i: nat).((pr0 t0 t1) \to
  42 ((getl i c (CHead d (Bind Abbr) u)) \to ((pr0 t0 t4) \to ((subst0 i u t4 t2)
  43 \to (ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2
  44 t))))))))))))))
  45 \def
  46  \lambda (c: C).(\lambda (d: C).(\lambda (t0: T).(\lambda (t1: T).(\lambda
  47 (t2: T).(\lambda (t4: T).(\lambda (u: T).(\lambda (i: nat).(\lambda (H: (pr0
  48 t0 t1)).(\lambda (H0: (getl i c (CHead d (Bind Abbr) u))).(\lambda (H1: (pr0
  49 t0 t4)).(\lambda (H2: (subst0 i u t4 t2)).(ex2_ind T (\lambda (t: T).(pr0 t4
  50 t)) (\lambda (t: T).(pr0 t1 t)) (ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda
  51 (t: T).(pr2 c t2 t))) (\lambda (x: T).(\lambda (H3: (pr0 t4 x)).(\lambda (H4:
  52 (pr0 t1 x)).(or_ind (pr0 t2 x) (ex2 T (\lambda (w2: T).(pr0 t2 w2)) (\lambda
  53 (w2: T).(subst0 i u x w2))) (ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t:
  54 T).(pr2 c t2 t))) (\lambda (H5: (pr0 t2 x)).(ex_intro2 T (\lambda (t: T).(pr2
  55 c t1 t)) (\lambda (t: T).(pr2 c t2 t)) x (pr2_free c t1 x H4) (pr2_free c t2
  56 x H5))) (\lambda (H5: (ex2 T (\lambda (w2: T).(pr0 t2 w2)) (\lambda (w2:
  57 T).(subst0 i u x w2)))).(ex2_ind T (\lambda (w2: T).(pr0 t2 w2)) (\lambda
  58 (w2: T).(subst0 i u x w2)) (ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t:
  59 T).(pr2 c t2 t))) (\lambda (x0: T).(\lambda (H6: (pr0 t2 x0)).(\lambda (H7:
  60 (subst0 i u x x0)).(ex_intro2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t:
  61 T).(pr2 c t2 t)) x0 (pr2_delta c d u i H0 t1 x H4 x0 H7) (pr2_free c t2 x0
  62 H6))))) H5)) (pr0_subst0 t4 x H3 u t2 i H2 u (pr0_refl u))))))
  63 (pr0_confluence t0 t4 H1 t1 H))))))))))))).
  64 (* COMMENTS
  65 Initial nodes: 403
  66 END *)
  67
  68 theorem pr2_confluence__pr2_delta_delta:
  69  \forall (c: C).(\forall (d: C).(\forall (d0: C).(\forall (t0: T).(\forall
  70 (t1: T).(\forall (t2: T).(\forall (t3: T).(\forall (t4: T).(\forall (u:
  71 T).(\forall (u0: T).(\forall (i: nat).(\forall (i0: nat).((getl i c (CHead d
  72 (Bind Abbr) u)) \to ((pr0 t0 t3) \to ((subst0 i u t3 t1) \to ((getl i0 c
  73 (CHead d0 (Bind Abbr) u0)) \to ((pr0 t0 t4) \to ((subst0 i0 u0 t4 t2) \to
  74 (ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2
  75 t))))))))))))))))))))
  76 \def
  77  \lambda (c: C).(\lambda (d: C).(\lambda (d0: C).(\lambda (t0: T).(\lambda
  78 (t1: T).(\lambda (t2: T).(\lambda (t3: T).(\lambda (t4: T).(\lambda (u:
  79 T).(\lambda (u0: T).(\lambda (i: nat).(\lambda (i0: nat).(\lambda (H: (getl i
  80 c (CHead d (Bind Abbr) u))).(\lambda (H0: (pr0 t0 t3)).(\lambda (H1: (subst0
  81 i u t3 t1)).(\lambda (H2: (getl i0 c (CHead d0 (Bind Abbr) u0))).(\lambda
  82 (H3: (pr0 t0 t4)).(\lambda (H4: (subst0 i0 u0 t4 t2)).(ex2_ind T (\lambda (t:
  83 T).(pr0 t4 t)) (\lambda (t: T).(pr0 t3 t)) (ex2 T (\lambda (t: T).(pr2 c t1
  84 t)) (\lambda (t: T).(pr2 c t2 t))) (\lambda (x: T).(\lambda (H5: (pr0 t4
  85 x)).(\lambda (H6: (pr0 t3 x)).(or_ind (pr0 t1 x) (ex2 T (\lambda (w2: T).(pr0
  86 t1 w2)) (\lambda (w2: T).(subst0 i u x w2))) (ex2 T (\lambda (t: T).(pr2 c t1
  87 t)) (\lambda (t: T).(pr2 c t2 t))) (\lambda (H7: (pr0 t1 x)).(or_ind (pr0 t2
  88 x) (ex2 T (\lambda (w2: T).(pr0 t2 w2)) (\lambda (w2: T).(subst0 i0 u0 x
  89 w2))) (ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t)))
  90 (\lambda (H8: (pr0 t2 x)).(ex_intro2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda
  91 (t: T).(pr2 c t2 t)) x (pr2_free c t1 x H7) (pr2_free c t2 x H8))) (\lambda
  92 (H8: (ex2 T (\lambda (w2: T).(pr0 t2 w2)) (\lambda (w2: T).(subst0 i0 u0 x
  93 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 t2 w2)) (\lambda (w2: T).(subst0 i0
  94 u0 x w2)) (ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t)))
  95 (\lambda (x0: T).(\lambda (H9: (pr0 t2 x0)).(\lambda (H10: (subst0 i0 u0 x
  96 x0)).(ex_intro2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t))
  97 x0 (pr2_delta c d0 u0 i0 H2 t1 x H7 x0 H10) (pr2_free c t2 x0 H9))))) H8))
  98 (pr0_subst0 t4 x H5 u0 t2 i0 H4 u0 (pr0_refl u0)))) (\lambda (H7: (ex2 T
  99 (\lambda (w2: T).(pr0 t1 w2)) (\lambda (w2: T).(subst0 i u x w2)))).(ex2_ind
 100 T (\lambda (w2: T).(pr0 t1 w2)) (\lambda (w2: T).(subst0 i u x w2)) (ex2 T
 101 (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t))) (\lambda (x0:
 102 T).(\lambda (H8: (pr0 t1 x0)).(\lambda (H9: (subst0 i u x x0)).(or_ind (pr0
 103 t2 x) (ex2 T (\lambda (w2: T).(pr0 t2 w2)) (\lambda (w2: T).(subst0 i0 u0 x
 104 w2))) (ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t)))
 105 (\lambda (H10: (pr0 t2 x)).(ex_intro2 T (\lambda (t: T).(pr2 c t1 t))
 106 (\lambda (t: T).(pr2 c t2 t)) x0 (pr2_free c t1 x0 H8) (pr2_delta c d u i H
 107 t2 x H10 x0 H9))) (\lambda (H10: (ex2 T (\lambda (w2: T).(pr0 t2 w2))
 108 (\lambda (w2: T).(subst0 i0 u0 x w2)))).(ex2_ind T (\lambda (w2: T).(pr0 t2
 109 w2)) (\lambda (w2: T).(subst0 i0 u0 x w2)) (ex2 T (\lambda (t: T).(pr2 c t1
 110 t)) (\lambda (t: T).(pr2 c t2 t))) (\lambda (x1: T).(\lambda (H11: (pr0 t2
 111 x1)).(\lambda (H12: (subst0 i0 u0 x x1)).(neq_eq_e i i0 (ex2 T (\lambda (t:
 112 T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t))) (\lambda (H13: (not (eq nat i
 113 i0))).(ex2_ind T (\lambda (t: T).(subst0 i u x1 t)) (\lambda (t: T).(subst0
 114 i0 u0 x0 t)) (ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2
 115 t))) (\lambda (x2: T).(\lambda (H14: (subst0 i u x1 x2)).(\lambda (H15:
 116 (subst0 i0 u0 x0 x2)).(ex_intro2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t:
 117 T).(pr2 c t2 t)) x2 (pr2_delta c d0 u0 i0 H2 t1 x0 H8 x2 H15) (pr2_delta c d
 118 u i H t2 x1 H11 x2 H14))))) (subst0_confluence_neq x x1 u0 i0 H12 x0 u i H9
 119 (sym_not_eq nat i i0 H13)))) (\lambda (H13: (eq nat i i0)).(let H14 \def
 120 (eq_ind_r nat i0 (\lambda (n: nat).(subst0 n u0 x x1)) H12 i H13) in (let H15
 121 \def (eq_ind_r nat i0 (\lambda (n: nat).(getl n c (CHead d0 (Bind Abbr) u0)))
 122 H2 i H13) in (let H16 \def (eq_ind C (CHead d (Bind Abbr) u) (\lambda (c0:
 123 C).(getl i c c0)) H (CHead d0 (Bind Abbr) u0) (getl_mono c (CHead d (Bind
 124 Abbr) u) i H (CHead d0 (Bind Abbr) u0) H15)) in (let H17 \def (f_equal C C
 125 (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
 126 \Rightarrow d | (CHead c0 _ _) \Rightarrow c0])) (CHead d (Bind Abbr) u)
 127 (CHead d0 (Bind Abbr) u0) (getl_mono c (CHead d (Bind Abbr) u) i H (CHead d0
 128 (Bind Abbr) u0) H15)) in ((let H18 \def (f_equal C T (\lambda (e: C).(match e
 129 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t)
 130 \Rightarrow t])) (CHead d (Bind Abbr) u) (CHead d0 (Bind Abbr) u0) (getl_mono
 131 c (CHead d (Bind Abbr) u) i H (CHead d0 (Bind Abbr) u0) H15)) in (\lambda
 132 (H19: (eq C d d0)).(let H20 \def (eq_ind_r T u0 (\lambda (t: T).(subst0 i t x
 133 x1)) H14 u H18) in (let H21 \def (eq_ind_r T u0 (\lambda (t: T).(getl i c
 134 (CHead d0 (Bind Abbr) t))) H16 u H18) in (let H22 \def (eq_ind_r C d0
 135 (\lambda (c0: C).(getl i c (CHead c0 (Bind Abbr) u))) H21 d H19) in (or4_ind
 136 (eq T x1 x0) (ex2 T (\lambda (t: T).(subst0 i u x1 t)) (\lambda (t:
 137 T).(subst0 i u x0 t))) (subst0 i u x1 x0) (subst0 i u x0 x1) (ex2 T (\lambda
 138 (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t))) (\lambda (H23: (eq T x1
 139 x0)).(let H24 \def (eq_ind T x1 (\lambda (t: T).(pr0 t2 t)) H11 x0 H23) in
 140 (ex_intro2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t)) x0
 141 (pr2_free c t1 x0 H8) (pr2_free c t2 x0 H24)))) (\lambda (H23: (ex2 T
 142 (\lambda (t: T).(subst0 i u x1 t)) (\lambda (t: T).(subst0 i u x0
 143 t)))).(ex2_ind T (\lambda (t: T).(subst0 i u x1 t)) (\lambda (t: T).(subst0 i
 144 u x0 t)) (ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t)))
 145 (\lambda (x2: T).(\lambda (H24: (subst0 i u x1 x2)).(\lambda (H25: (subst0 i
 146 u x0 x2)).(ex_intro2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c
 147 t2 t)) x2 (pr2_delta c d u i H22 t1 x0 H8 x2 H25) (pr2_delta c d u i H22 t2
 148 x1 H11 x2 H24))))) H23)) (\lambda (H23: (subst0 i u x1 x0)).(ex_intro2 T
 149 (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t)) x0 (pr2_free c t1
 150 x0 H8) (pr2_delta c d u i H22 t2 x1 H11 x0 H23))) (\lambda (H23: (subst0 i u
 151 x0 x1)).(ex_intro2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2
 152 t)) x1 (pr2_delta c d u i H22 t1 x0 H8 x1 H23) (pr2_free c t2 x1 H11)))
 153 (subst0_confluence_eq x x1 u i H20 x0 H9))))))) H17)))))))))) H10))
 154 (pr0_subst0 t4 x H5 u0 t2 i0 H4 u0 (pr0_refl u0)))))) H7)) (pr0_subst0 t3 x
 155 H6 u t1 i H1 u (pr0_refl u)))))) (pr0_confluence t0 t4 H3 t3
 156 H0))))))))))))))))))).
 157 (* COMMENTS
 158 Initial nodes: 1901
 159 END *)
 160
 161 theorem pr2_confluence:
 162  \forall (c: C).(\forall (t0: T).(\forall (t1: T).((pr2 c t0 t1) \to (\forall
 163 (t2: T).((pr2 c t0 t2) \to (ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t:
 164 T).(pr2 c t2 t))))))))
 165 \def
 166  \lambda (c: C).(\lambda (t0: T).(\lambda (t1: T).(\lambda (H: (pr2 c t0
 167 t1)).(\lambda (t2: T).(\lambda (H0: (pr2 c t0 t2)).(let H1 \def (match H in
 168 pr2 return (\lambda (c0: C).(\lambda (t: T).(\lambda (t3: T).(\lambda (_:
 169 (pr2 c0 t t3)).((eq C c0 c) \to ((eq T t t0) \to ((eq T t3 t1) \to (ex2 T
 170 (\lambda (t4: T).(pr2 c t1 t4)) (\lambda (t4: T).(pr2 c t2 t4)))))))))) with
 171 [(pr2_free c0 t3 t4 H1) \Rightarrow (\lambda (H2: (eq C c0 c)).(\lambda (H3:
 172 (eq T t3 t0)).(\lambda (H4: (eq T t4 t1)).(eq_ind C c (\lambda (_: C).((eq T
 173 t3 t0) \to ((eq T t4 t1) \to ((pr0 t3 t4) \to (ex2 T (\lambda (t: T).(pr2 c
 174 t1 t)) (\lambda (t: T).(pr2 c t2 t))))))) (\lambda (H5: (eq T t3 t0)).(eq_ind
 175 T t0 (\lambda (t: T).((eq T t4 t1) \to ((pr0 t t4) \to (ex2 T (\lambda (t5:
 176 T).(pr2 c t1 t5)) (\lambda (t5: T).(pr2 c t2 t5)))))) (\lambda (H6: (eq T t4
 177 t1)).(eq_ind T t1 (\lambda (t: T).((pr0 t0 t) \to (ex2 T (\lambda (t5:
 178 T).(pr2 c t1 t5)) (\lambda (t5: T).(pr2 c t2 t5))))) (\lambda (H7: (pr0 t0
 179 t1)).(let H8 \def (match H0 in pr2 return (\lambda (c1: C).(\lambda (t:
 180 T).(\lambda (t5: T).(\lambda (_: (pr2 c1 t t5)).((eq C c1 c) \to ((eq T t t0)
 181 \to ((eq T t5 t2) \to (ex2 T (\lambda (t6: T).(pr2 c t1 t6)) (\lambda (t6:
 182 T).(pr2 c t2 t6)))))))))) with [(pr2_free c1 t5 t6 H8) \Rightarrow (\lambda
 183 (H9: (eq C c1 c)).(\lambda (H10: (eq T t5 t0)).(\lambda (H11: (eq T t6
 184 t2)).(eq_ind C c (\lambda (_: C).((eq T t5 t0) \to ((eq T t6 t2) \to ((pr0 t5
 185 t6) \to (ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2
 186 t))))))) (\lambda (H12: (eq T t5 t0)).(eq_ind T t0 (\lambda (t: T).((eq T t6
 187 t2) \to ((pr0 t t6) \to (ex2 T (\lambda (t7: T).(pr2 c t1 t7)) (\lambda (t7:
 188 T).(pr2 c t2 t7)))))) (\lambda (H13: (eq T t6 t2)).(eq_ind T t2 (\lambda (t:
 189 T).((pr0 t0 t) \to (ex2 T (\lambda (t7: T).(pr2 c t1 t7)) (\lambda (t7:
 190 T).(pr2 c t2 t7))))) (\lambda (H14: (pr0 t0
 191 t2)).(pr2_confluence__pr2_free_free c t0 t1 t2 H7 H14)) t6 (sym_eq T t6 t2
 192 H13))) t5 (sym_eq T t5 t0 H12))) c1 (sym_eq C c1 c H9) H10 H11 H8)))) |
 193 (pr2_delta c1 d u i H8 t5 t6 H9 t H10) \Rightarrow (\lambda (H11: (eq C c1
 194 c)).(\lambda (H12: (eq T t5 t0)).(\lambda (H13: (eq T t t2)).(eq_ind C c
 195 (\lambda (c2: C).((eq T t5 t0) \to ((eq T t t2) \to ((getl i c2 (CHead d
 196 (Bind Abbr) u)) \to ((pr0 t5 t6) \to ((subst0 i u t6 t) \to (ex2 T (\lambda
 197 (t7: T).(pr2 c t1 t7)) (\lambda (t7: T).(pr2 c t2 t7))))))))) (\lambda (H14:
 198 (eq T t5 t0)).(eq_ind T t0 (\lambda (t7: T).((eq T t t2) \to ((getl i c
 199 (CHead d (Bind Abbr) u)) \to ((pr0 t7 t6) \to ((subst0 i u t6 t) \to (ex2 T
 200 (\lambda (t8: T).(pr2 c t1 t8)) (\lambda (t8: T).(pr2 c t2 t8))))))))
 201 (\lambda (H15: (eq T t t2)).(eq_ind T t2 (\lambda (t7: T).((getl i c (CHead d
 202 (Bind Abbr) u)) \to ((pr0 t0 t6) \to ((subst0 i u t6 t7) \to (ex2 T (\lambda
 203 (t8: T).(pr2 c t1 t8)) (\lambda (t8: T).(pr2 c t2 t8))))))) (\lambda (H16:
 204 (getl i c (CHead d (Bind Abbr) u))).(\lambda (H17: (pr0 t0 t6)).(\lambda
 205 (H18: (subst0 i u t6 t2)).(pr2_confluence__pr2_free_delta c d t0 t1 t2 t6 u i
 206 H7 H16 H17 H18)))) t (sym_eq T t t2 H15))) t5 (sym_eq T t5 t0 H14))) c1
 207 (sym_eq C c1 c H11) H12 H13 H8 H9 H10))))]) in (H8 (refl_equal C c)
 208 (refl_equal T t0) (refl_equal T t2)))) t4 (sym_eq T t4 t1 H6))) t3 (sym_eq T
 209 t3 t0 H5))) c0 (sym_eq C c0 c H2) H3 H4 H1)))) | (pr2_delta c0 d u i H1 t3 t4
 210 H2 t H3) \Rightarrow (\lambda (H4: (eq C c0 c)).(\lambda (H5: (eq T t3
 211 t0)).(\lambda (H6: (eq T t t1)).(eq_ind C c (\lambda (c1: C).((eq T t3 t0)
 212 \to ((eq T t t1) \to ((getl i c1 (CHead d (Bind Abbr) u)) \to ((pr0 t3 t4)
 213 \to ((subst0 i u t4 t) \to (ex2 T (\lambda (t5: T).(pr2 c t1 t5)) (\lambda
 214 (t5: T).(pr2 c t2 t5))))))))) (\lambda (H7: (eq T t3 t0)).(eq_ind T t0
 215 (\lambda (t5: T).((eq T t t1) \to ((getl i c (CHead d (Bind Abbr) u)) \to
 216 ((pr0 t5 t4) \to ((subst0 i u t4 t) \to (ex2 T (\lambda (t6: T).(pr2 c t1
 217 t6)) (\lambda (t6: T).(pr2 c t2 t6)))))))) (\lambda (H8: (eq T t t1)).(eq_ind
 218 T t1 (\lambda (t5: T).((getl i c (CHead d (Bind Abbr) u)) \to ((pr0 t0 t4)
 219 \to ((subst0 i u t4 t5) \to (ex2 T (\lambda (t6: T).(pr2 c t1 t6)) (\lambda
 220 (t6: T).(pr2 c t2 t6))))))) (\lambda (H9: (getl i c (CHead d (Bind Abbr)
 221 u))).(\lambda (H10: (pr0 t0 t4)).(\lambda (H11: (subst0 i u t4 t1)).(let H12
 222 \def (match H0 in pr2 return (\lambda (c1: C).(\lambda (t5: T).(\lambda (t6:
 223 T).(\lambda (_: (pr2 c1 t5 t6)).((eq C c1 c) \to ((eq T t5 t0) \to ((eq T t6
 224 t2) \to (ex2 T (\lambda (t7: T).(pr2 c t1 t7)) (\lambda (t7: T).(pr2 c t2
 225 t7)))))))))) with [(pr2_free c1 t5 t6 H12) \Rightarrow (\lambda (H13: (eq C
 226 c1 c)).(\lambda (H14: (eq T t5 t0)).(\lambda (H15: (eq T t6 t2)).(eq_ind C c
 227 (\lambda (_: C).((eq T t5 t0) \to ((eq T t6 t2) \to ((pr0 t5 t6) \to (ex2 T
 228 (\lambda (t7: T).(pr2 c t1 t7)) (\lambda (t7: T).(pr2 c t2 t7))))))) (\lambda
 229 (H16: (eq T t5 t0)).(eq_ind T t0 (\lambda (t7: T).((eq T t6 t2) \to ((pr0 t7
 230 t6) \to (ex2 T (\lambda (t8: T).(pr2 c t1 t8)) (\lambda (t8: T).(pr2 c t2
 231 t8)))))) (\lambda (H17: (eq T t6 t2)).(eq_ind T t2 (\lambda (t7: T).((pr0 t0
 232 t7) \to (ex2 T (\lambda (t8: T).(pr2 c t1 t8)) (\lambda (t8: T).(pr2 c t2
 233 t8))))) (\lambda (H18: (pr0 t0 t2)).(ex2_sym T (pr2 c t2) (pr2 c t1)
 234 (pr2_confluence__pr2_free_delta c d t0 t2 t1 t4 u i H18 H9 H10 H11))) t6
 235 (sym_eq T t6 t2 H17))) t5 (sym_eq T t5 t0 H16))) c1 (sym_eq C c1 c H13) H14
 236 H15 H12)))) | (pr2_delta c1 d0 u0 i0 H12 t5 t6 H13 t7 H14) \Rightarrow
 237 (\lambda (H15: (eq C c1 c)).(\lambda (H16: (eq T t5 t0)).(\lambda (H17: (eq T
 238 t7 t2)).(eq_ind C c (\lambda (c2: C).((eq T t5 t0) \to ((eq T t7 t2) \to
 239 ((getl i0 c2 (CHead d0 (Bind Abbr) u0)) \to ((pr0 t5 t6) \to ((subst0 i0 u0
 240 t6 t7) \to (ex2 T (\lambda (t8: T).(pr2 c t1 t8)) (\lambda (t8: T).(pr2 c t2
 241 t8))))))))) (\lambda (H18: (eq T t5 t0)).(eq_ind T t0 (\lambda (t8: T).((eq T
 242 t7 t2) \to ((getl i0 c (CHead d0 (Bind Abbr) u0)) \to ((pr0 t8 t6) \to
 243 ((subst0 i0 u0 t6 t7) \to (ex2 T (\lambda (t9: T).(pr2 c t1 t9)) (\lambda
 244 (t9: T).(pr2 c t2 t9)))))))) (\lambda (H19: (eq T t7 t2)).(eq_ind T t2
 245 (\lambda (t8: T).((getl i0 c (CHead d0 (Bind Abbr) u0)) \to ((pr0 t0 t6) \to
 246 ((subst0 i0 u0 t6 t8) \to (ex2 T (\lambda (t9: T).(pr2 c t1 t9)) (\lambda
 247 (t9: T).(pr2 c t2 t9))))))) (\lambda (H20: (getl i0 c (CHead d0 (Bind Abbr)
 248 u0))).(\lambda (H21: (pr0 t0 t6)).(\lambda (H22: (subst0 i0 u0 t6
 249 t2)).(pr2_confluence__pr2_delta_delta c d d0 t0 t1 t2 t4 t6 u u0 i i0 H9 H10
 250 H11 H20 H21 H22)))) t7 (sym_eq T t7 t2 H19))) t5 (sym_eq T t5 t0 H18))) c1
 251 (sym_eq C c1 c H15) H16 H17 H12 H13 H14))))]) in (H12 (refl_equal C c)
 252 (refl_equal T t0) (refl_equal T t2)))))) t (sym_eq T t t1 H8))) t3 (sym_eq T
 253 t3 t0 H7))) c0 (sym_eq C c0 c H4) H5 H6 H1 H2 H3))))]) in (H1 (refl_equal C
 254 c) (refl_equal T t0) (refl_equal T t1)))))))).
 255 (* COMMENTS
 256 Initial nodes: 2087
 257 END *)
 258