proposition: Lemma sn_preimage T1 T2 (e1 : T1 -> T1 -> Prop) (e2 : T2 -> T2 -> Prop) (h : T1 -> T2) x : (forall x y, e1 x y -> e2 (h x) (h y)) -> sn e2 (h x) -> sn e1 x.
proof: Proof. move eqn:(h x) => v A B. elim: B h x A eqn => {v} - v _ ih h x A eqn. apply: SN => y /A. rewrite eqn => /ih; eauto. Qed.
imports: Relations Recdef mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base)