-theorem lift_app: ∀M,N,k,p.
- lift (App M N) k p = App (lift M k p) (lift N k p).
-// qed.
-
-theorem lift_lambda: ∀N,M,k,p. lift (Lambda N M) k p =
- Lambda (lift N k p) (lift M (k + 1) p).
-// qed.
-
-theorem lift_prod: ∀N,M,k,p.
- lift (Prod N M) k p = Prod (lift N k p) (lift M (k + 1) p).
-// qed.
-
-(* telescopic non-delifting substitution of l in M.
- * [this is the telescoping delifting substitution lifted by |l|]
- * Rel 0 is replaced with the head of l
- *)
-let rec substc M l on l ≝ match l with
- [ nil ⇒ M
- | cons A D ⇒ (lift (substc M[0≝A] D) 0 1)
- ].
-
-interpretation "Substc" 'Subst1 M l = (substc M l).
-
-(* this is just to test that substitution works as expected
-theorem test1: ∀A,B,C. (App (App (Rel 0) (Rel 1)) (Rel 2))[A::B::C::nil ?] =
- App (App (lift A 0 1) (lift B 0 2)) (lift C 0 3).
-#A #B #C normalize
->lift_0 >lift_0 >lift_0
->lift_lift1>lift_lift1>lift_lift1>lift_lift1>lift_lift1>lift_lift1
-normalize
+lemma all2_nth: ∀A,B:Type[0]. ∀P:A→B→Prop. ∀a,b. P a b →
+ ∀i,l1,l2. all2 … P l1 l2 → P (nth i … l1 a) (nth i … l2 b).
+#A #B #P #a #b #Hab #i elim i -i [ @all2_hd // | #i #IH #l1 #l2 #H @IH /2/ ]