proposition: Lemma retract_fin_incl : forall P Q f, retract_fin P f -> incl Q P -> retract_fin Q f.
proof: Proof. unfold retract_fin; intros. apply (H Q0 FQ); auto. apply incl_trans with Q; auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)