added lemmas is_Var_mgu_if_not_in_equations, ball_is_Var_mgu, and inj_on_mgu
Description
Description
Details
Details
- Provenance
desharna Authored on - Parents
- rAFP4b6f5ef48a74: RealTimeDeque: replace `reverseN` with `take_rev
- Branches
- Unknown
- Tags
added lemmas is_Var_mgu_if_not_in_equations, ball_is_Var_mgu, and inj_on_mgu Tags None Subscribers None |