proposition: Lemma in_record_bounded : forall (a : E) (f : E1), Bounded.axioms (in_record a f).
proof: Proof. ir. ap Bounded.criterion. apply ex_intro with (IM (recordMap (a:=a) (f:=f))). ir. ap IM_inc. ap in_record_ex. am. Qed.
imports: set_theory