Diffusion afp-devel d67e01cbf88e

added lemma subst_compose_apply_eq_apply_lhs_if
d67e01cbf88e
Actions

Tags

None

Subscribers

None

Description

added lemma subst_compose_apply_eq_apply_lhs_if

Details

Provenance

Authored on

Parents

rAFP4cb61705b37c: added lemmas is_Var_mgu_if_not_in_equations, ball_is_Var_mgu, and inj_on_mgu

Branches

Unknown

Tags

Unknown

Event Timeline

desharna committed rAFPd67e01cbf88e: added lemma subst_compose_apply_eq_apply_lhs_if.Nov 10 2022, 10:32 PM

Changes (1)

Path

Size

thys/

First_Order_Terms/

rAFPd67e01cbf88e

thys/First_Order_Terms/Term.thy

Loading...