proposition: Lemma abstract_i_compatible : forall i e e', snd(abstract_i i e) = Some e' -> compatible e e'.
proof: Proof. induction i; simpl; intros e e'. intros Heq; injection Heq; intro; subst e'; apply compatible_update. assert (IHi1' := IHi1 e). destruct (abstract_i i1 e) as [i'1 [e1 | ]]; simpl in IHi1'. assert (IHi2' := IHi2 e1). destruct (abstract_i i2 e1) as [i'2 [e2 | ]]; simpl in IHi2'; intros Heq. injection Heq; intro; subst e'; apply compatible_trans with e1; auto. discriminate Heq. intros; discriminate. destruct (intersect_env true e b). case_eq (fp e b i (abstract_i i)); intros i' [l'' | ] Hfp Hi. apply compatible_trans with l''. apply fp_compatible with (2:= Hfp). exact IHi. apply compatible_intersect_env with false b; auto. apply compatible_intersect_env with false b; auto. intros Heq; injection Heq; intro; subst e'; apply compatible_refl. intros Heq; injection Heq; intro; subst e'; apply compatible_refl. Qed.
imports: syntax little denot Bool List String ZArith axiom