proposition: Lemma appUnits_subst_length : forall M G (MG: correct_subst M G), isFunS (appHead M) -> length (appUnits (subst MG)) = length (appUnits M).
proof: Proof. intro M; destruct M as [E Pt T M]; induction M; try_solve; intros. rewrite appUnits_notApp; trivial. intro MGapp. assert (forall M, isApp M -> isFunS M -> False). intro M; term_inv M. apply H0 with (subst MG); trivial. apply funS_subst_funS; trivial. rewrite (appUnits_app (buildT (TApp M1 M2)) I). rewrite (appUnits_app (subst MG) (app_subst_app (M:=buildT (TApp M1 M2)) I MG)). autorewrite with datatypes using simpl. destruct (app_subst (M:=buildT (TApp M1 M2)) I MG). rewrite H0. rewrite <- (IHM1 G (subst_appL_c (M:=buildT (TApp M1 M2)) I MG)); trivial. set (w := @appHead_left (buildT (TApp M1 M2)) I); auto. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)