proposition: Lemma lgmap_avatar_create : forall f g u, is_leq_gen_scale f u -> lgmap f g u = Function.create u (avatar f g).
proof: Proof. ir. util (Function.create_recovers (f:=lgmap f g u)). assert (is_leq_gen_mapping f g (lgmap f g u)). ap lgmap_lgmapping. am. uh H0; ee; am. wr H0. ap Function.create_extensionality. rw lgmap_domain. tv. am. ir. ap lgmap_avatar. am. am. Qed.
imports: Arith order