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, 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 | 138 |