proposition: Lemma idSubst_decl0 M A (M0: env M |= 0 := A) : idSubst M = {x/buildT (TVar M0)}.
proof: Proof. destruct M as [envM ???]; simpl. destruct (isVarDecl_dec envM 0) as [[B EB] | En]. replace (buildT (TVar EB)) with (buildT (TVar M0)); trivial. apply term_eq; trivial. exfalso; apply varD_UD_absurd with envM 0 A; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)