proposition: Lemma subst_dom_varSubst_rev : forall G x A, subst_dom G |= x := A -> exists T, G |-> x/T /\ type T = A.
proof: Proof. induction G. destruct x; try_solve. intros x A Gx. destruct x. destruct a. inversion Gx. exists t; fo. try_solve. inversion Gx. destruct (IHG x A H0). exists x0; fo. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)