Theorem relation.refl_gen.to_refl_trans_gen
Modification history
2022-01-27 23:05
src/logic/relation.lean
feat(order/succ_pred/relation): `succ`/`pred` inductions on relations (#11518) …
Modified relation.refl_gen.to_refl_trans_genView on Github →2021-08-23 10:17
src/logic/relation.lean
docs(logic/relation): add module docstring (#8773) …
Modified relation.refl_gen.to_refl_trans_genView on Github →