proposition: Lemma typing_activeEnv : forall M, activeEnv M |- term M := type M.
proof: Proof. destruct M as [E Pt T M]. induction M; simpl. constructor 1. unfold VarD; rewrite nth_app_right; autorewrite with datatypes. replace (x - x) with 0; trivial. lia. lia. constructor. constructor. fold (activeEnv (buildT M)). apply typing_ext_env with (activeEnv (buildT M)); trivial. intros x C MAx. assert (forall C, activeEnv (buildT M) |= 0 := C -> A = C). intros; set (w := activeEnv_subset (buildT M) H). inversion w; trivial. destruct (activeEnv (buildT M)). inversion MAx; destruct x; try_solve. destruct x; try_solve. rewrite (H C); trivial. constructor. constructor 4 with A. apply typing_ext_env_r; trivial. apply (activeEnv_app_comp (buildT (TApp M1 M2)) I). apply typing_ext_env_l; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)