nat_compl:
Simplify proof. ord_compl: Add def incrF_S. WIP: incrF_equiv. Finite_family: Proof of injF_restr_bij_EX.
Loading
Please register or sign in to comment
Simplify proof. ord_compl: Add def incrF_S. WIP: incrF_equiv. Finite_family: Proof of injF_restr_bij_EX.