proposition: Lemma avatar_refl : forall f x, leq_gen f x x -> avatar f f x = x.
proof: Proof. ir. rewrite <- avatar_char with (a:= fun (i:E) => i). tv. ir. assert (Image.create (chenille f x0) (fun i : E => i) = (chenille f x0)). ap extensionality; uhg; ir. rwi Image.inc_rw H1. nin H1. ee. wr H2; am. rw Image.inc_rw. sh x1; ee; try am; try tv. rw H1. rw chenille_next. tv. am. am. Qed.
imports: Arith order