-lemma lift_rel_ge: ∀i,p,k. (S i) ≰ k → lift (Rel i) k p = Rel (i+p).
-#i #p #k #Hik normalize >(lt_to_leb_false (S i) k) /2/
-qed.
-
-lemma lift_app: ∀M,N,k,p.
- lift (App M N) k p = App (lift M k p) (lift N k p).
-// qed.
-
-lemma lift_lambda: ∀N,M,k,p. lift (Lambda N M) k p =
- Lambda (lift N k p) (lift M (k + 1) p).
-// qed.
-
-lemma lift_prod: ∀N,M,k,p.
- lift (Prod N M) k p = Prod (lift N k p) (lift M (k + 1) p).
-// qed.
-
-lemma subst_app: ∀M,N,k,L. (App M N)[k≝L] = App M[k≝L] N[k≝L].
-// qed.
-
-lemma subst_lambda: ∀N,M,k,L. (Lambda N M)[k≝L] = Lambda N[k≝L] M[k+1≝L].
-// qed.
-
-lemma subst_prod: ∀N,M,k,L. (Prod N M)[k≝L] = Prod N[k≝L] M[k+1≝L].
-// qed.
-
-
-axiom lift_subst_lt: ∀A,B,i,j,k. lift (B[j≝A]) (j+k) i =
- (lift B (j+k+1) i)[j≝lift A k i].
-
-(* telescopic delifting substitution of l in M.
- * Rel 0 is replaced with the head of l
- *)
-let rec tsubst M l on l ≝ match l with
- [ nil ⇒ M
- | cons A D ⇒ (tsubst M[0≝A] D)
- ].
-
-interpretation "telescopic substitution" 'Subst1 M l = (tsubst M l).
-
-lemma tsubst_refl: ∀l,t. (lift t 0 (|l|))[l] = t.
-#l (elim l) -l (normalize) // #hd #tl #IHl #t cut (S (|tl|) = |tl| + 1) // (**) (* eliminate cut *)
+lemma all2_append: ∀A,B,P,l2,m2. all2 A B P l2 m2 →
+ ∀l1,m1. all2 A B P l1 m1 → all2 A B P (l1 @ l2) (m1 @ m2).
+#A #B #P #l2 #m2 #H2 #l1 (elim l1) -l1 [ #m1 #H >H @H2 ]
+#x1 #l1 #IH1 #m2 elim m2 -m2 [ #false elim false ]
+#x2 #m2 #_ #H elim H -H /3/