include "basic_1/wf3/defs.ma".
-let rec wf3_ind (g: G) (P: (C \to (C \to Prop))) (f: (\forall (m: nat).(P
-(CSort m) (CSort m)))) (f0: (\forall (c1: C).(\forall (c2: C).((wf3 g c1 c2)
-\to ((P c1 c2) \to (\forall (u: T).(\forall (t: T).((ty3 g c1 u t) \to
+implied rec lemma wf3_ind (g: G) (P: (C \to (C \to Prop))) (f: (\forall (m:
+nat).(P (CSort m) (CSort m)))) (f0: (\forall (c1: C).(\forall (c2: C).((wf3 g
+c1 c2) \to ((P c1 c2) \to (\forall (u: T).(\forall (t: T).((ty3 g c1 u t) \to
(\forall (b: B).(P (CHead c1 (Bind b) u) (CHead c2 (Bind b) u))))))))))) (f1:
(\forall (c1: C).(\forall (c2: C).((wf3 g c1 c2) \to ((P c1 c2) \to (\forall
(u: T).(((\forall (t: T).((ty3 g c1 u t) \to False))) \to (\forall (b: B).(P
((wf3_ind g P f f0 f1 f2) c1 c2 w0) u f3 b) | (wf3_flat c1 c2 w0 u f3)
\Rightarrow (f2 c1 c2 w0 ((wf3_ind g P f f0 f1 f2) c1 c2 w0) u f3)].
-theorem wf3_gen_sort1:
+lemma wf3_gen_sort1:
\forall (g: G).(\forall (x: C).(\forall (m: nat).((wf3 g (CSort m) x) \to
(eq C x (CSort m)))))
\def
[(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I (CSort m)
H3) in (False_ind (eq C c2 (CHead c1 (Flat f) u)) H4))))))))) y x H0))) H)))).
-theorem wf3_gen_bind1:
+lemma wf3_gen_bind1:
\forall (g: G).(\forall (c1: C).(\forall (x: C).(\forall (v: T).(\forall (b:
B).((wf3 g (CHead c1 (Bind b) v) x) \to (or (ex3_2 C T (\lambda (c2:
C).(\lambda (_: T).(eq C x (CHead c2 (Bind b) v)))) (\lambda (c2: C).(\lambda
(\lambda (_: C).(\forall (w: T).((ty3 g c1 v w) \to False))))) H4))))))))) y
x H0))) H)))))).
-theorem wf3_gen_flat1:
+lemma wf3_gen_flat1:
\forall (g: G).(\forall (c1: C).(\forall (x: C).(\forall (v: T).(\forall (f:
F).((wf3 g (CHead c1 (Flat f) v) x) \to (wf3 g c1 x))))))
\def
\def (eq_ind C c0 (\lambda (c: C).(wf3 g c c2)) H1 c1 H8) in H10))))) H5))
H4))))))))) y x H0))) H)))))).
-theorem wf3_gen_head2:
+lemma wf3_gen_head2:
\forall (g: G).(\forall (x: C).(\forall (c: C).(\forall (v: T).(\forall (k:
K).((wf3 g x (CHead c k v)) \to (ex B (\lambda (b: B).(eq K k (Bind b)))))))))
\def