proposition: Lemma eq_units_eq_terms : forall M N, appUnits M = appUnits N -> M = N.
proof: Proof. intro M. apply well_founded_ind with (R := subterm) (P := fun M => forall N, appUnits M = appUnits N -> M = N ). apply subterm_wf. clear M; intros M IH N unitsEq. case (isApp_dec M); case (isApp_dec N). intros Napp Mapp. rewrite (appUnits_app M Mapp) in unitsEq. rewrite (appUnits_app N Napp) in unitsEq. destruct (app_inj_tail (appUnits (appBodyL Mapp)) (appUnits (appBodyL Napp)) (appBodyR Mapp) (appBodyR Napp)); trivial. apply app_eq with Mapp Napp; simpl. apply IH; trivial. constructor 1 with Mapp; constructor 2. trivial. intros; exfalso. apply app_notApp_diffUnits with M N; trivial. intros; exfalso. apply app_notApp_diffUnits with N M; auto. intros Nnapp Mnapp. do 2 rewrite appUnits_notApp in unitsEq; trivial. congruence. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)