proposition: Lemma avatar_leq_gen : forall f g x y, is_expansive g -> leq_gen f x y -> leq_gen g (avatar f g x) (avatar f g y).
proof: Proof. ir. apply by_cases with (x = y); ir. rw H1. ap avatar_leq_gen_def. rwi H1 H0. am. assert (inc (avatar f g x) (chenille g (avatar f g y))). rw avatar_chenille. rw Image.inc_rw. sh x; ee; try tv. rw chenille_inc. ee; am. apply leq_gen_def2 with x. am. am. apply leq_gen_def2 with x. am. rwi chenille_inc H2; ee. am. ap avatar_leq_gen_def. apply leq_gen_def2 with x. am. Qed.
imports: Arith order