proposition: Lemma appUnit_conv_appUnit : forall M M' N Q, M ~(Q) N -> isAppUnit M' M -> exists N', isAppUnit N' N /\ M' ~(Q) N'.
proof: Proof. intros. destruct (list_In_nth (appUnits M) M' H0) as [p Mp]. set (MNunits := appUnits_conv H). destruct (list_sim_nth p MNunits Mp) as [N' [Np M'N']]. exists N'; split; trivial. unfold isAppUnit; apply nth_some_in with p; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)