proposition: Lemma activeEnv_subset : forall M, envSubset (activeEnv M) (env M).
proof: Proof. destruct M as [E Pt T M]; induction M; simpl; intros; intros x0 A0 H. inversion H. destruct (@activeEnv_var_det (buildT (TVar v)) x x0 A0); trivial. rewrite H2; rewrite H0; trivial. destruct x0; try_solve. fold (activeEnv (buildT M)) in H. assert (activeEnv (buildT M) |= S x0 := A0). destruct (activeEnv (buildT M)); try_solve. destruct x0; try_solve. set (w := IHM (S x0) A0 H0). inversion w; trivial. fold (activeEnv (buildT M1)) in H. fold (activeEnv (buildT M2)) in H. destruct (env_sum_varDecl (activeEnv (buildT M1)) (activeEnv (buildT M2)) H) as [[DL _] | DR]. apply IHM1; trivial. apply IHM2; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)