proposition: Lemma slack_ind (T : choiceType) (P : {fset T} -> Type) (U : {fset T}): (forall X, (forall Y, Y `<=` U -> X `<` Y -> P Y) -> X `<=` U -> P X)-> forall X, X `<=` U -> P X.
proof: Proof. move => H. apply (nat_size_ind (f := fun X => size U - size X) (P := fun X => X `<=` U -> P X)). move => X IH. apply: H => Y inU. move/proper_size => H. apply: IH (inU). apply: ltn_sub2l => //. apply: leq_trans H _. exact: subset_size. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)