proposition: Lemma envSubst_transp_twice : forall S, envSubst_transp (envSubst_transp S) <=> S.
proof: Proof. intro S; constructor; intros i j; destruct S; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)