proposition: Lemma fp1_invariant_init : forall e l b i f i', compatible e l -> fp1 e l b i f = (i', Some l) -> fp1 l l b i f = (i', Some l).
proof: Proof. intros e l b i f i' Hc; unfold fp1. destruct (intersect_env true l b); try (simpl; auto; fail). destruct (f a) as [i'' [ l'' | ]]; try (intros; discriminate). intros Heq; injection Heq; intros Hl Hi'; subst i'; clear Heq. rewrite <- Hl. rewrite join_env_assoc; rewrite join_env_involutive; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom