proposition: Lemma fp1_compatible : forall f e l1 b i1 i' l2, (forall l l', snd (f l) = Some l' -> compatible l l') -> compatible e l1 -> fp1 e l1 b i1 f = (i', Some l2) -> compatible e l1 -> compatible e l2.
proof: Proof. intros f e l1 b i1 i' l2 Hf Hcel1; unfold fp1. case_eq (intersect_env true l1 b); [intros l' Hi | intros Hi]. case_eq (f l'); intros a_i [l'' | ] Hfl' Heq. injection Heq; do 2 intro; subst i' l2. intros; apply compatible_join_env_left. apply compatible_trans with l1; auto. apply compatible_trans with l'; auto. apply compatible_intersect_env with true b; auto. apply compatible_join_env_left. apply Hf; rewrite Hfl'; auto. discriminate. intros Heq; injection Heq; do 2 intro; subst i' l2; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom