proposition: Lemma fp1_abstract_i_body_imp_invariant : forall e l b i1 f i2 i3 l1 l2 l3, (forall l l', snd (f l) = Some l' -> compatible l l') -> compatible e l -> intersect_env true l b = Some l1 -> f l1 = (i3, Some l3) -> fp1 e l b i1 f = (i2, Some l2) -> thinner_env l3 l2.
proof: Proof. intros e l b i1 f i2 i3 l1 l2 l3 Hfc Hcel Hi Hf. unfold fp1; rewrite Hi; rewrite Hf. assert (compatible l l1) by (apply compatible_intersect_env with true b; auto). assert (compatible l1 l3) by (apply Hfc; rewrite Hf; auto). intros Heq; injection Heq; do 2 intro; subst i2 l2. apply thinner_env_trans with (join_env l1 l3). apply thinner_join_env_right. apply compatible_sym. apply Hfc; rewrite Hf; auto. apply thinner_join_env_right. apply compatible_sym; apply compatible_trans with l; auto. apply compatible_trans with l1; auto. apply compatible_join_env_left; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom