proposition: Lemma envSubst_eq_def : forall S1 S2 i j, S1 <=> S2 -> (envSub S1 i j <-> envSub S2 i j).
proof: Proof. intros; destruct H; split; intro. apply (H0 i j H1). apply (H i j H1). Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)