IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.EtaCompletionM0a

declarations in this module (23)

• def crossDiff L39
• theorem crossDiff_self L43
• theorem crossDiff_of_crossEq L48
• theorem crossDiff_swap L55
• theorem crossDiff_triangle_id L63
• structure RegularSeq L74
• def equiv L83
• theorem eta_regular L89
• def eta L96
• theorem eta_seq L100
• theorem equiv_refl L104
• theorem equiv_symm L113
• theorem equiv_trans L128
• theorem eta_respects_crossEq L196
• theorem equiv_equivalence L207
• def equivSetoid L215
• def RealDelta L222
• def mk L228
• theorem mk_eq_mk_of_equiv L232
• def etaQ L241
• theorem etaQ_mk L246
• theorem crossEq_of_equiv_eta L253
• theorem etaQ_injective L275