proposition: Lemma fp2_widen2_eq_fp1 : forall e b i i', fp1 (widen2 e)(widen2 e) b i (abstract_i i) = (i', Some (widen2 e)) -> fp2 (widen2 e)(widen2 e) b i (abstract_i i) = found i' (Some(widen2 e)).
proof: Proof. intros e b i i' Hfp1; unfold fp2; repeat rewrite Hfp1; rewrite stable_refl; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom