proposition: Lemma finite_tack_on_case : forall x y f, is_finite x -> Transformation.injective (tack_on x y) (tack_on x y) f -> f y = y -> Transformation.bijective (tack_on x y) (tack_on x y) f.
proof: Proof. ir. uhg; ee; try lu. apply by_cases with (inc y x); ir. assert (tack_on x y = x). ap extensionality; uhg; ir. rwi tack_on_inc H3; nin H3. am. rw H3; am. rw tack_on_inc. ap or_introl; am. rw H3. rwi H3 H0. cp (H f H0). lu. util (H f). uhg; ee. uhg; ir. uh H0; ee. util (H0 x0). rw tack_on_inc; ap or_introl; am. rwi tack_on_inc H5; nin H5. am. assert (x0 = y). ap H4. rw tack_on_inc. ap or_introl; am. rw tack_on_inc; ap or_intror; tv. rw H5; sy; am. assert False. ap H2. wr H6; am. elim H7. uh H0; ee. uhg; ir. ap H3. rw tack_on_inc; ap or_introl; am. rw tack_on_inc; ap or_introl; am. am. uhg; ee; try lu. uhg; ir. rwi tack_on_inc H4; nin H4. uh H3; ee. uh H5; ee. cp (H7 _ H4). nin H8. ee. sh x1. ee; try am. rw tack_on_inc; ap or_introl; am. sh y; ee. rw tack_on_inc; ap or_intror; tv. rw H4. am. Qed.
imports: Arith ordinal