Theory MiniFormulas_Sema

theory MiniFormulas_Sema
imports MiniFormulas Sema
begin

lemma "A ⊨ F ⟷ A ⊨ to_mini_formula F"
  by(induction F) auto

end