Theoremslist_chain', append, append_overlap, chain, cons', cons_of_le, cons_of_ne_nil, drop, getElem, iff, iff_mem, imp, induction, infix, init, iterate_eq_of_apply_eq, left_of_append, prefix, rel_head, rel_head?, right_of_append, sublist, suffix, tail, take, backwards_induction, backwards_induction_head, iff, iff_mem, induction, pairwise, rel, sublist, 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, chain', chain'_append, chain'_append_cons_cons, chain'_attach, chain'_attachWith, chain'_cons', chain'_cons_cons, chain'_eq_iff_eq_replicate, chain'_flatten, chain'_iff_forall_getElem, chain'_iff_forall_rel_of_append_cons_cons, chain'_iff_get, chain'_iff_pairwise, chain'_isInfix, chain'_map, chain'_map_of_chain', chain'_nil, chain'_of_chain'_map, chain'_of_not, chain'_pair, chain'_reverse, chain'_singleton, chain'_split, chain_append_cons_cons, chain_append_singleton_iff_forall₂, chain_eq_iff_eq_replicate, chain_iff, chain_iff_forall₂, chain_iff_get, chain_iff_pairwise, chain_map, chain_map_of_chain, chain_of_chain_map, chain_of_chain_pmap, chain_pmap_of_chain, chain_replicate_of_rel, chain_singleton, chain_split, exists_chain_of_relationReflTransGen, 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_chain_cons, relationReflTransGen_of_exists_isChain, relationReflTransGen_of_exists_isChain_cons, list_chain', instIsWellFoundedChainsLex_chains | 155 |