Mv extF_widenF_S from Finite_family to ord_compl.
Proofs of extF_ind_{l,r} (= aliases for extF_lift_S and extF_widenF_S). Hide admits, that are actually not used.
Loading
Please register or sign in to comment
Proofs of extF_ind_{l,r} (= aliases for extF_lift_S and extF_widenF_S). Hide admits, that are actually not used.