buildMembershipLL Show Code edit
thm (buildMembershipLL () (H (= B0 B1)) (↔ (∈ A B0) (∈ A B1))
H
(= B0 B1)
B0 B1 A MembershipBuilderLL
(→ (= B0 B1) (↔ (∈ A B0) (∈ A B1)))
applyModusPonens
(↔ (∈ A B0) (∈ A B1))
)
edit