+(* substitution lemma arity assignment *)
+(* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
+lemma aa_subst: ∀v,E,t,Ek. 〚t[|Ek|≝v]〛_[Ek @ E] = 〚t〛_[Ek @ 〚v〛_[E]::E].
+#v #E #t (elim t) -t
+ [ //
+ | #i #Ek @(leb_elim (S i) (|Ek|)) #H1ik
+ [ >(aa_rel_lt … H1ik) >(subst_rel1 … H1ik) >(aa_rel_lt … H1ik) //
+ | @(eqb_elim i (|Ek|)) #H2ik
+ [ >(aa_rel_ge … H1ik) >H2ik -H2ik H1ik >subst_rel2
+ >(aa_lift ? ? ? ([])) <minus_n_n /2/
+ | (lapply (arith4 … H1ik H2ik)) -H1ik H2ik #Hik
+ (>(subst_rel3 … Hik)) (>aa_rel_ge) [2: /2/ ]
+ <(associative_append ? ? ([?]) ?)
+ >aa_rel_ge >length_append (>commutative_plus)
+ [ <minus_plus // | @not_le_to_not_le_S_S /2/ ]
+ ]
+ ]
+ | //
+ | #N #M #IHN #IHM #Ek >subst_lambda > aa_lambda
+ >commutative_plus >(IHM (? :: ?)) /3/
+ | #N #M #IHN #IHM #Ek >subst_prod > aa_prod
+ >commutative_plus >(IHM (? :: ?)) /4/
+ | #M #IHM #Ek @IHM
+qed.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+