proposition: Lemma fp2_invariant : forall e e' b i f l i', (forall e e', snd(f e) = Some e' -> compatible e e') -> compatible e e' -> fp2 e e' b i f = found i' (Some l) -> fp2 l l b i f = found i' (Some l).
proof: Proof. intros e e' b i f l i' Hf Hce'; unfold fp2. case_eq (fp1 e e' b i f); intros i1 l1 Heqfp1; destruct l1 as [l1 | ]; try(intros; discriminate). case_eq (fp1 e l1 b i f); intros i2 l2 Heqfp1_2; destruct l2 as [l2 | ]; try(intros; discriminate). case_eq (stable l1 l2); intros Hstable; try (intros; discriminate). intros Heq; injection Heq; do 2 intro; subst i2 l1; clear Heq. assert (compatible e l) by (apply fp1_compatible with (f:=f) (l1:=e')(i1:=i)(b:=b)(i':=i1); auto). assert (l = l2). apply compatible_stable_eq; auto. apply compatible_trans with e. apply compatible_sym; auto. apply fp1_compatible with (f:=f) (l1:=l)(i1:=i)(b:=b)(i':=i'); auto. subst l2. rewrite fp1_invariant_init with (2:=Heqfp1_2); auto. rewrite fp1_invariant_init with (2:=Heqfp1_2); auto. rewrite Hstable; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom