proposition: Lemma fp_compatible : forall e b i f i' l', (forall e e', snd(f e) = Some e' -> compatible e e') -> fp e b i f = (i', Some l') -> compatible e l'.
proof: Proof. intros e b i f i' l' Hf. unfold fp. case_eq (fp2 e e b i f); [intros a_i [l1 | ] Hfp2 Heq | intros l1 Hfp2]. injection Heq; do 2 intro; subst i' l'. apply fp2_compatible with (2:= Hfp2); auto. apply compatible_refl. discriminate. case_eq (fp2 e l1 b i f);[intros a_i' [l2 | ] Hfp2' Heq | intros l2 Hfp2']. injection Heq; do 2 intro; subst i' l'. apply fp2_compatible with (2:=Hfp2'); auto. apply fp2_compatible2 with (2:= Hfp2); auto. apply compatible_refl. discriminate. case_eq (fp1 (widen2 e)(widen2 e) b i f); intros a_i [l3 | ] Hfp1 Heq. injection Heq; do 2 intro; subst i' l'. apply compatible_widen2. discriminate. Qed.
imports: syntax little denot Bool List String ZArith axiom