proposition: Lemma subst_ran_decl : forall G x A, subst_ran G |= x := A -> exists T p, G |-> p/T /\ env T |= x := A.
proof: Proof. induction G. destruct x; try_solve. intros. destruct a. rewrite subst_ran_cons_some in H. destruct (env_sum_varDecl (env t) (subst_ran G) H) as [[Tx Gx] | Gx]. exists t; exists 0; split; compute; trivial. destruct (IHG x A Gx) as [T [p [Gp Tx]]]. exists T; exists (S p); split; trivial. rewrite subst_ran_cons_none in H. destruct (IHG x A H) as [T [p [Gp Tx]]]. exists T; exists (S p); split; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)