proposition: Lemma fp2_precondition1 : forall e l b i1 i2 i' l', compatible e l -> fp2 e l b i1 (abstract_i i2) = found i' (Some l') -> forall g, i_a Ab.m g (a_conj (a_b b)(to_a l')) -> i_a Ab.m g (pc i' (to_a l')).
proof: Proof. intros e l b i1 i2 i' l' Hcel. unfold fp2. case_eq (fp1 e l b i1 (abstract_i i2)); intros i3 [l'1 | ] Hfp1. assert (Hcel'1 : compatible e l'1). apply fp1_compatible with (3:= Hfp1); auto. exact (abstract_i_compatible i2). case_eq (fp1 e l'1 b i1 (abstract_i i2)); intros i4 [l'2 | ] Hfp1'. assert (Hcel'2 : compatible e l'2). apply fp1_compatible with (3:= Hfp1'); auto. exact (abstract_i_compatible i2). case_eq (stable l'1 l'2); intros Hst Heq. injection Heq; do 2 intro; subst l'1 i4; clear Heq. intros g Ha; apply precondition_shift with (a:= (to_a l'2)). rewrite compatible_stable_eq with (2:= Hst); auto. apply compatible_trans with e; auto; apply compatible_sym; auto. apply fp1_precondition with (2:= Hfp1'); auto. discriminate. intros; discriminate. intros; discriminate. Qed.
imports: syntax little denot Bool List String ZArith axiom