proposition: Lemma fp_monotonic_entry : forall g e b i1 i2 i3 l, fp e b i1 (abstract_i i2) = (i3, Some l) -> i_a Ab.m g (to_a e) -> i_a Ab.m g (to_a l).
proof: Proof. intros g e b i1 i2 i3 l H. apply thinner_env_to_a. apply fp_thinner with (f:= abstract_i i2) (2:=H). exact (abstract_i_compatible i2). Qed.
imports: syntax little denot Bool List String ZArith axiom