Theorem: SetTheory.interpret_subset (SetTheory/Formula.lean)

State before:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
n✝ : Nat
x y : α✝ ⊕ Fin n✝
v : α✝ → V
l : Fin n✝ → V
⊢ Interpret V (BoundedFormula.subset x y) v l ↔ interpretTerm V v l x ⊆ interpretTerm V v l y
Tactic:
unfold BoundedFormula.subset
State after:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
n✝ : Nat
x y : α✝ ⊕ Fin n✝
v : α✝ → V
l : Fin n✝ → V
⊢ Interpret V
      (BoundedFormula.all
        (BoundedFormula.imp (BoundedFormula.mem (Sum.inr (Fin.last n✝)) (termSucc x))
          (BoundedFormula.mem (Sum.inr (Fin.last n✝)) (termSucc y))))
      v l ↔
    interpretTerm V v l x ⊆ interpretTerm V v l y

State before:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
n✝ : Nat
x y : α✝ ⊕ Fin n✝
v : α✝ → V
l : Fin n✝ → V
⊢ Interpret V
      (BoundedFormula.all
        (BoundedFormula.imp (BoundedFormula.mem (Sum.inr (Fin.last n✝)) (termSucc x))
          (BoundedFormula.mem (Sum.inr (Fin.last n✝)) (termSucc y))))
      v l ↔
    interpretTerm V v l x ⊆ interpretTerm V v l y
Tactic:
aesop
State after:
no goals