-let rec clear_ind (P: (C \to (C \to Prop))) (f: (\forall (b: B).(\forall (e:
-C).(\forall (u: T).(P (CHead e (Bind b) u) (CHead e (Bind b) u)))))) (f0:
-(\forall (e: C).(\forall (c: C).((clear e c) \to ((P e c) \to (\forall (f0:
-F).(\forall (u: T).(P (CHead e (Flat f0) u) c)))))))) (c: C) (c0: C) (c1:
-clear c c0) on c1: P c c0 \def match c1 with [(clear_bind b e u) \Rightarrow
-(f b e u) | (clear_flat e c2 c3 f1 u) \Rightarrow (f0 e c2 c3 ((clear_ind P f
-f0) e c2 c3) f1 u)].
+implied rec lemma clear_ind (P: (C \to (C \to Prop))) (f: (\forall (b:
+B).(\forall (e: C).(\forall (u: T).(P (CHead e (Bind b) u) (CHead e (Bind b)
+u)))))) (f0: (\forall (e: C).(\forall (c: C).((clear e c) \to ((P e c) \to
+(\forall (f0: F).(\forall (u: T).(P (CHead e (Flat f0) u) c)))))))) (c: C)
+(c0: C) (c1: clear c c0) on c1: P c c0 \def match c1 with [(clear_bind b e u)
+\Rightarrow (f b e u) | (clear_flat e c2 c3 f1 u) \Rightarrow (f0 e c2 c3
+((clear_ind P f f0) e c2 c3) f1 u)].