proposition: Lemma next_compatible_avatar : forall a f g x, next_compatible f a -> inc x (U a) -> avatar f g x = avatar (next a) g x.
proof: Proof. ir. cp H; uh H; ee. util (wo_induction (a:= a) H (p:= (fun x => avatar f g x = avatar (next a) g x))). ir. rw avatar_image_chenille. rw avatar_image_chenille. ap uneq. ap extensionality; uhg; ir. rwi Image.inc_rw H5. rw Image.inc_rw. nin H5. sh x2; xd. rewrite chenille_punctured_downward with (a:= a). rewrite chenille_punctured_downward with (a:=a) in H5. am. am. am. ap next_compatible_next; am. am. wr H4. am. rewrite chenille_punctured_downward with (a:=a) in H5. ufi punctured_downward_subset H5; Ztac. am. am. rewrite chenille_punctured_downward with (a:=a) in H5. ufi punctured_downward_subset H5; Ztac. am. am. rwi Image.inc_rw H5. rw Image.inc_rw. nin H5. sh x2; xd. rewrite chenille_punctured_downward with (a:= a). rewrite chenille_punctured_downward with (a:=a) in H5. am. ap next_compatible_next; am. am. am. am. rw H4. am. rewrite chenille_punctured_downward with (a:=a) in H5. ufi punctured_downward_subset H5; Ztac. ap next_compatible_next. am. am. rewrite chenille_punctured_downward with (a:=a) in H5. ufi punctured_downward_subset H5; Ztac. ap next_compatible_next. am. am. rw next_leq_gen_leq. ap leq_refl; try lu. am. am. am. rewrite leq_gen_leq with (a:=a). ap leq_refl; lu. am. am. am. exact (H3 _ H0). Qed.
imports: Arith order