Theoremslist_chain', append, append_overlap, backwards_concat_induction, backwards_cons_induction, backwards_cons_induction_head, backwards_induction, concat_induction, concat_induction_head, cons, cons', cons_induction, cons_of_le, cons_of_ne_nil, drop, dropLast, iff, iff_mem, iff_mem_mem_tail, iff_of_mem_imp, iff_of_mem_tail_imp, imp_head, imp_of_mem_imp, imp_of_mem_tail_imp, induction, infix, isChain_cons, iterate_eq_of_apply_eq, left_of_append, prefix, rel_cons, rel_head, rel_head?, right_of_append, sublist, suffix, tail, take, exists_isChain_cons_of_relationReflTransGen, exists_isChain_ne_nil_of_relationReflTransGen, exists_not_getElem_of_not_isChain, isChain_append, isChain_append_cons_cons, isChain_attach, isChain_attachWith, isChain_cons, isChain_cons', isChain_cons_append_cons_cons, isChain_cons_append_singleton_iff_forall₂, isChain_cons_eq_iff_eq_replicate, isChain_cons_iff, isChain_cons_iff_forall₂, isChain_cons_iff_get, isChain_cons_map, isChain_cons_map_of_isChain_cons, isChain_cons_of_isChain_cons_map, isChain_cons_of_isChain_cons_pmap, isChain_cons_pmap, isChain_cons_pmap_of_isChain_cons, isChain_cons_split, isChain_eq_iff_eq_replicate, isChain_flatten, isChain_iff, isChain_iff_forall_rel_of_append_cons_cons, isChain_iff_forall₂, isChain_iff_get, isChain_isInfix, isChain_map, isChain_map_of_isChain, isChain_nil, isChain_of_isChain_map, isChain_of_isChain_pmap, isChain_pair, isChain_pmap, isChain_pmap_of_isChain, isChain_replicate_of_rel, isChain_reverse, isChain_singleton, isChain_split, relationReflTransGen_of_exists_isChain, relationReflTransGen_of_exists_isChain_cons, list_chain', instIsWellFoundedChainsLex_chains | 83 |