+(* Basic eliminators ********************************************************)
+
+lemma isfin_ind (R:predicate rtmap): (∀f. 𝐈❪f❫ → R f) →
+ (∀f. 𝐅❪f❫ → R f → R (⫯f)) →
+ (∀f. 𝐅❪f❫ → R f → R (↑f)) →
+ ∀f. 𝐅❪f❫ → R f.
+#R #IH1 #IH2 #IH3 #f #H elim H -H
+#n #H elim H -f -n /3 width=2 by ex_intro/
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma isfin_inv_push: ∀g. 𝐅❪g❫ → ∀f. ⫯f = g → 𝐅❪f❫.
+#g * /3 width=4 by fcla_inv_px, ex_intro/
+qed-.
+
+lemma isfin_inv_next: ∀g. 𝐅❪g❫ → ∀f. ↑f = g → 𝐅❪f❫.
+#g * #n #H #f #H0 elim (fcla_inv_nx … H … H0) -g
+/2 width=2 by ex_intro/
+qed-.
+