proposition: Lemma lgmap_avatar : forall f g u x, is_leq_gen_scale f u -> inc x u -> V x (lgmap f g u) = avatar f g x.
proof: Proof. ir. ap leq_gen_mapping_avatar. ap lgmap_lgmapping. am. rw lgmap_domain. am. am. Qed.
imports: Arith order