induction h2 generalizing V
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2 : IsConv E F F'
⊢ Holds D I V M E F ↔ Holds D I V M E F'
case conv_refl
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
phi✝ : Formula
V : Valuation D
⊢ Holds D I V M E phi✝ ↔ Holds D I V M E phi✝

case conv_symm
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
phi✝ phi'✝ : Formula
a✝ : IsConv E phi✝ phi'✝
a_ih✝ : ∀ (V : Valuation D), Holds D I V M E phi✝ ↔ Holds D I V M E phi'✝
V : Valuation D
⊢ Holds D I V M E phi'✝ ↔ Holds D I V M E phi✝

case conv_trans
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
phi✝ phi'✝ phi''✝ : Formula
a✝¹ : IsConv E phi✝ phi'✝
a✝ : IsConv E phi'✝ phi''✝
a_ih✝¹ : ∀ (V : Valuation D), Holds D I V M E phi✝ ↔ Holds D I V M E phi'✝
a_ih✝ : ∀ (V : Valuation D), Holds D I V M E phi'✝ ↔ Holds D I V M E phi''✝
V : Valuation D
⊢ Holds D I V M E phi✝ ↔ Holds D I V M E phi''✝

case conv_not
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
phi✝ phi'✝ : Formula
a✝ : IsConv E phi✝ phi'✝
a_ih✝ : ∀ (V : Valuation D), Holds D I V M E phi✝ ↔ Holds D I V M E phi'✝
V : Valuation D
⊢ Holds D I V M E phi✝.not_ ↔ Holds D I V M E phi'✝.not_

case conv_imp
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
phi✝ phi'✝ psi✝ psi'✝ : Formula
a✝¹ : IsConv E phi✝ phi'✝
a✝ : IsConv E psi✝ psi'✝
a_ih✝¹ : ∀ (V : Valuation D), Holds D I V M E phi✝ ↔ Holds D I V M E phi'✝
a_ih✝ : ∀ (V : Valuation D), Holds D I V M E psi✝ ↔ Holds D I V M E psi'✝
V : Valuation D
⊢ Holds D I V M E (phi✝.imp_ psi✝) ↔ Holds D I V M E (phi'✝.imp_ psi'✝)

case conv_forall
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
x✝ : VarName
phi✝ phi'✝ : Formula
a✝ : IsConv E phi✝ phi'✝
a_ih✝ : ∀ (V : Valuation D), Holds D I V M E phi✝ ↔ Holds D I V M E phi'✝
V : Valuation D
⊢ Holds D I V M E (forall_ x✝ phi✝) ↔ Holds D I V M E (forall_ x✝ phi'✝)

case conv_unfold
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d✝ : Definition
σ✝ : Instantiation
a✝ : d✝ ∈ E
V : Valuation D
⊢ Holds D I V M E (def_ d✝.name (List.map (↑σ✝) d✝.args)) ↔ Holds D I V M E (sub σ✝ meta_var_ d✝.F)