proposition: Lemma avatar_trans : forall f g h x, is_expansive g -> leq_gen f x x -> avatar g h (avatar f g x) = avatar f h x.
proof: Proof. ir. util (chenille_induction (f:=f) (p:= fun z => avatar g h (avatar f g z) = avatar f h z)). ir. set (u:= avatar f g x0). rw avatar_image_chenille. rw avatar_image_chenille. ap uneq. uf u. rw avatar_chenille. rw Image.trans. ap Image.same. tv. ir. ap H2. am. am. am. am. uf u. ap avatar_leq_gen_def. am. ap H1. am. Qed.
imports: Arith order