proposition: Lemma envMinimal_abs : forall M N (Mabs: isAbs M), term (absBody Mabs) = term N -> tail (env (absBody Mabs)) = tail (env N) -> (env N |= 0 :! \/ env N |= 0 := absType Mabs) -> envMinimal N -> envMinimal M.
proof: Proof. unfold envMinimal; intros. rewrite (activeEnv_abs M Mabs). rewrite (@activeEnv_minimal (absBody Mabs) N); trivial. rewrite <- H2. rewrite <- H0. rewrite absBody_env; trivial. rewrite absBody_env. destruct (env N). apply env_comp_empty. unfold decl; apply env_comp_cons. rewrite absBody_env in H0. simpl in H0; rewrite H0; auto with terms. destruct o; auto. destruct H1; inversion H1; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)