-let rec drop_ind (P: (nat \to (nat \to (C \to (C \to Prop))))) (f: (\forall
-(c: C).(P O O c c))) (f0: (\forall (k: K).(\forall (h: nat).(\forall (c:
-C).(\forall (e: C).((drop (r k h) O c e) \to ((P (r k h) O c e) \to (\forall
-(u: T).(P (S h) O (CHead c k u) e))))))))) (f1: (\forall (k: K).(\forall (h:
-nat).(\forall (d: nat).(\forall (c: C).(\forall (e: C).((drop h (r k d) c e)
-\to ((P h (r k d) c e) \to (\forall (u: T).(P h (S d) (CHead c k (lift h (r k
-d) u)) (CHead e k u))))))))))) (n: nat) (n0: nat) (c: C) (c0: C) (d: drop n
-n0 c c0) on d: P n n0 c c0 \def match d with [(drop_refl c1) \Rightarrow (f
-c1) | (drop_drop k h c1 e d0 u) \Rightarrow (f0 k h c1 e d0 ((drop_ind P f f0
-f1) (r k h) O c1 e d0) u) | (drop_skip k h d0 c1 e d1 u) \Rightarrow (f1 k h
-d0 c1 e d1 ((drop_ind P f f0 f1) h (r k d0) c1 e d1) u)].
+implied rec lemma drop_ind (P: (nat \to (nat \to (C \to (C \to Prop))))) (f:
+(\forall (c: C).(P O O c c))) (f0: (\forall (k: K).(\forall (h: nat).(\forall
+(c: C).(\forall (e: C).((drop (r k h) O c e) \to ((P (r k h) O c e) \to
+(\forall (u: T).(P (S h) O (CHead c k u) e))))))))) (f1: (\forall (k:
+K).(\forall (h: nat).(\forall (d: nat).(\forall (c: C).(\forall (e: C).((drop
+h (r k d) c e) \to ((P h (r k d) c e) \to (\forall (u: T).(P h (S d) (CHead c
+k (lift h (r k d) u)) (CHead e k u))))))))))) (n: nat) (n0: nat) (c: C) (c0:
+C) (d: drop n n0 c c0) on d: P n n0 c c0 \def match d with [(drop_refl c1)
+\Rightarrow (f c1) | (drop_drop k h c1 e d0 u) \Rightarrow (f0 k h c1 e d0
+((drop_ind P f f0 f1) (r k h) O c1 e d0) u) | (drop_skip k h d0 c1 e d1 u)
+\Rightarrow (f1 k h d0 c1 e d1 ((drop_ind P f f0 f1) h (r k d0) c1 e d1) u)].