Theorem: lengthOfEqualSets (Bml/Setsimp.lean)

State before:
X Y : Finset Formula
⊢ X = Y → lengthOfSet X = lengthOfSet Y
Tactic:
intro hyp
State after:
X Y : Finset Formula
hyp : X = Y
⊢ lengthOfSet X = lengthOfSet Y

State before:
X Y : Finset Formula
hyp : X = Y
⊢ lengthOfSet X = lengthOfSet Y
Tactic:
aesop
State after:
no goals