Theoremsadd, casesOn', casesOn1, const, id, mul, of_eq, pow, prec1, pred, sub, swap, swap', mem_range_encode, prim, and, beq, bind_decode_iff, comp, comp₂, cond, const, decode, decode₂, dom_bool, dom_bool₂, dom_denumerable, dom_finite, dom_fintype, encdec, encode, encode_iff, eq, fin_succ, fin_val, fin_val_iff, fst, id, ite, list_findIdx₁, list_getElem?₁, list_idxOf₁, map_decode_iff, nat_add, nat_bodd, nat_casesOn, nat_casesOn', nat_casesOn₁, nat_div, nat_div2, nat_double, nat_double_succ, nat_findGreatest, nat_iff, nat_iterate, nat_le, nat_lt, nat_max, nat_min, nat_mod, nat_mul, nat_rec, nat_rec', nat_rec₁, nat_sub, not, ofNat, ofNat_iff, of_eq, of_equiv, of_equiv_iff, of_equiv_symm, of_equiv_symm_iff, of_graph, option_bind, option_bind₁, option_casesOn, option_get, option_getD, option_getD_default, option_guard, option_iget, option_isSome, option_map, option_map₁, option_orElse, option_some, option_some_iff, or, pair, pred, primrecPred, snd, subtype_mk, subtype_val, subtype_val_iff, succ, sumCasesOn, sumInl, sumInr, to₂, ulower_down, ulower_up, unpair, and, comp, decide, not, of_eq, or, primrecRel, comp, comp₂, decide, not, of_eq, swap, comp, comp₂, const, curry, encode_iff, left, mk, natPair, nat_iff, nat_iff', ofNat_iff, of_eq, option_some_iff, pair, primrecRel, right, swap, uncurry, unpaired, unpaired', primrecPred_iff_primrec_decide, primrecRel_iff_primrec_decide | 139 |