proposition: Lemma envSub_minimal_rev : forall Q M M' x y, envSub_minimal Q M -> M ~(Q) M' -> envSub Q x y -> exists A, activeEnv M' |= y := A.
proof: Proof. intros Q M M' x y QMmin MM' Qxy. destruct (QMmin x y Qxy). exists x0. apply (proj1 ((proj2 MM') x y Qxy x0)); trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)