proposition: Lemma terms_conv_activeEnv_rev : forall N M Q, M ~(Q) N -> forall q A, activeEnv N |= q := A -> exists p, envSub Q p q.
proof: Proof. intros. inversion H. set (NM := terms_conv_sym_aux H). destruct (terms_conv_activeEnv NM H0). exists x. destruct Q; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)