proposition: Lemma mult_lifting : forall (r : relation A), (forall x x' y y', x =A= x' -> y =A= y' -> r x y -> r x' y') -> (forall l x x', In x' l -> x =A= x' -> In x l) -> forall l, Accs r l -> Restricted_acc (Accs r) (mult (transp r)) l.
proof: Proof. intros r C1 C2 l Accs_l. elim (Restricted_acc_eq_acc (Accs r) (mult (transp r)) l); intros H1 H2. apply H1; clear H1 H2. apply Inclusion.Acc_incl with (mult (transp r)). intros a b H; elim H; trivial. apply HAccTermsToTermlist; trivial. unfold transp; simpl; intros x x' y y' Hxy Hx'y'. apply (C1 y y' x x'); trivial. Qed.
imports: Coq(List Permutation Arith Morphisms Basics) CoLoR(MultisetOrder RelExtras MultisetCore MultisetList MultisetTheory AccUtil RelUtil LogicUtil) CoLoR(AccUtil ListUtil)