induction F
F : Formula
V : VarBoolAssignment
h1 : F.IsPrime
⊢ evalPrime V F = (V F = true)
case pred_const_
V : VarBoolAssignment
a✝¹ : PredName
a✝ : List VarName
h1 : (pred_const_ a✝¹ a✝).IsPrime
⊢ evalPrime V (pred_const_ a✝¹ a✝) = (V (pred_const_ a✝¹ a✝) = true)

case pred_var_
V : VarBoolAssignment
a✝¹ : PredName
a✝ : List VarName
h1 : (pred_var_ a✝¹ a✝).IsPrime
⊢ evalPrime V (pred_var_ a✝¹ a✝) = (V (pred_var_ a✝¹ a✝) = true)

case eq_
V : VarBoolAssignment
a✝¹ a✝ : VarName
h1 : (eq_ a✝¹ a✝).IsPrime
⊢ evalPrime V (eq_ a✝¹ a✝) = (V (eq_ a✝¹ a✝) = true)

case true_
V : VarBoolAssignment
h1 : true_.IsPrime
⊢ evalPrime V true_ = (V true_ = true)

case false_
V : VarBoolAssignment
h1 : false_.IsPrime
⊢ evalPrime V false_ = (V false_ = true)

case not_
V : VarBoolAssignment
a✝ : Formula
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : a✝.not_.IsPrime
⊢ evalPrime V a✝.not_ = (V a✝.not_ = true)

case imp_
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.IsPrime → evalPrime V a✝¹ = (V a✝¹ = true)
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : (a✝¹.imp_ a✝).IsPrime
⊢ evalPrime V (a✝¹.imp_ a✝) = (V (a✝¹.imp_ a✝) = true)

case and_
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.IsPrime → evalPrime V a✝¹ = (V a✝¹ = true)
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : (a✝¹.and_ a✝).IsPrime
⊢ evalPrime V (a✝¹.and_ a✝) = (V (a✝¹.and_ a✝) = true)

case or_
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.IsPrime → evalPrime V a✝¹ = (V a✝¹ = true)
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : (a✝¹.or_ a✝).IsPrime
⊢ evalPrime V (a✝¹.or_ a✝) = (V (a✝¹.or_ a✝) = true)

case iff_
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.IsPrime → evalPrime V a✝¹ = (V a✝¹ = true)
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : (a✝¹.iff_ a✝).IsPrime
⊢ evalPrime V (a✝¹.iff_ a✝) = (V (a✝¹.iff_ a✝) = true)

case forall_
V : VarBoolAssignment
a✝¹ : VarName
a✝ : Formula
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : (forall_ a✝¹ a✝).IsPrime
⊢ evalPrime V (forall_ a✝¹ a✝) = (V (forall_ a✝¹ a✝) = true)

case exists_
V : VarBoolAssignment
a✝¹ : VarName
a✝ : Formula
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : (exists_ a✝¹ a✝).IsPrime
⊢ evalPrime V (exists_ a✝¹ a✝) = (V (exists_ a✝¹ a✝) = true)

case def_
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ evalPrime V (def_ a✝¹ a✝) = (V (def_ a✝¹ a✝) = true)