proposition: Lemma avatar_char : forall f g a y, (forall x, leq_gen f x x -> a x = g (Image.create (chenille f x) a)) -> leq_gen f y y -> a y = avatar f g y.
proof: Proof. ir. util (leq_gen_induction (f:= f) (p:= fun z => a z = avatar f g z)). ir. rw avatar_image_chenille. rw H. assert (forall e f, e=f -> (g e = g f)). ir. rw H3. tv. ap H3. ap Image.same. tv. ir. ap H2. rwi chenille_inc H4. xd. am. rwi chenille_inc H4; xd. am. am. ap H1. am. Qed.
imports: Arith order