proposition: Lemma avatar_leq_gen_def : forall f g x, leq_gen f x x -> leq_gen g (avatar f g x) (avatar f g x).
proof: Proof. ir. rwi leq_gen_char H. ee. nin H. ap leq_gen_def_char. sh (Image.create x0 (avatar f g)). ee. ap lgs_avatar_image. am. rw Image.inc_rw. sh x. ee; try am; try tv. Qed.
imports: Arith order