simp only [Holds]
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi psi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
psi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E psi → (Holds D I V M E' psi ↔ Holds D I V M E psi)
V : Valuation D
h2_left : IsMetaVarOrAllDefInEnv E phi
h2_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I V M E' (phi.imp_ psi) ↔ Holds D I V M E (phi.imp_ psi)
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi psi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
psi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E psi → (Holds D I V M E' psi ↔ Holds D I V M E psi)
V : Valuation D
h2_left : IsMetaVarOrAllDefInEnv E phi
h2_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I V M E' phi → Holds D I V M E' psi ↔ Holds D I V M E phi → Holds D I V M E psi