+lemma lift_subst_up: ∀M,N,n,i,j.
+ lift M[i≝N] (i+j) n = (lift M (i+j+1) n)[i≝ (lift N j n)].
+#M (elim M)
+ [//
+ |#p #N #n #i #j (cases (true_or_false (leb p i)))
+ [#lepi (cases (le_to_or_lt_eq … (leb_true_to_le … lepi)))
+ [#ltpi >(subst_rel1 … ltpi)
+ (cut (p < i+j)) [@(lt_to_le_to_lt … ltpi) //] #ltpij
+ >(lift_rel_lt … ltpij); >(lift_rel_lt ?? p ?);
+ [>subst_rel1 // | @(lt_to_le_to_lt … ltpij) //]
+ |#eqpi >eqpi >subst_rel2 >lift_rel_lt;
+ [>subst_rel2 >(plus_n_O (i+j))
+ applyS lift_lift_up
+ |@(le_to_lt_to_lt ? (i+j)) //
+ ]
+ ]
+ |#lefalse (cut (i < p)) [@not_le_to_lt /2/] #ltip
+ (cut (0 < p)) [@(le_to_lt_to_lt … ltip) //] #posp
+ >(subst_rel3 … ltip) (cases (true_or_false (leb (S p) (i+j+1))))
+ [#Htrue (cut (p < i+j+1)) [@(leb_true_to_le … Htrue)] #Hlt
+ >lift_rel_lt;
+ [>lift_rel_lt // >(subst_rel3 … ltip) // | @lt_plus_to_minus //]
+ |#Hfalse >lift_rel_ge;
+ [>lift_rel_ge;
+ [>subst_rel3; [@eq_f /2/ | @(lt_to_le_to_lt … ltip) //]
+ |@not_lt_to_le @(leb_false_to_not_le … Hfalse)
+ ]
+ |@le_plus_to_minus_r @not_lt_to_le
+ @(leb_false_to_not_le … Hfalse)
+ ]
+ ]
+ ]
+ |#P #Q #HindP #HindQ #N #n #i #j normalize
+ @eq_f2; [@HindP |@HindQ ]
+ |#P #Q #HindP #HindQ #N #n #i #j normalize
+ @eq_f2; [@HindP |>associative_plus >(commutative_plus j 1)
+ <associative_plus @HindQ]
+ |#P #Q #HindP #HindQ #N #n #i #j normalize
+ @eq_f2; [@HindP |>associative_plus >(commutative_plus j 1)
+ <associative_plus @HindQ]
+ |#P #HindP #N #n #i #j normalize
+ @eq_f @HindP
+ ]
+qed.
+
+lemma lift_subst_up_O: ∀v,t,k,p. (lift t (k+1) p)[O≝lift v k p] = lift t[O≝v] k p.
+// qed.
+