proposition: Lemma appUnits_conv : forall M N Q, M ~(Q) N -> conv_list (appUnits M) (appUnits N) Q.
proof: Proof. intro M. apply well_founded_ind with (R := subterm) (P := fun M => forall N Q, M ~(Q) N -> conv_list (appUnits M) (appUnits N) Q). apply subterm_wf. clear M; intros M IH N Q MN. destruct (isApp_dec M) as [Mapp | Mnapp]. set (Napp := proj1 (isApp_morph (conv_by MN)) Mapp). rewrite (appUnits_app M Mapp). rewrite (appUnits_app N Napp). unfold conv_list; apply list_sim_app. apply IH. apply appBodyL_subterm. apply app_conv_app_left_aux; trivial. constructor. apply app_conv_app_right_aux; trivial. constructor. rewrite !appUnits_notApp; trivial. constructor; trivial. constructor. rewrite <- (conv_by MN); trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)