Conditions missing in final lemma output

[Airini]

For some cases, the condition found to make a property hold is not included in the output lemma, even though the lemma proven to hold is the conditioned version.

eg.: with the usual naturals Nat, leq and

fun lezP :: "Nat ⇒ bool" where
  "lezP Z = True"
| "lezP _ = False"

the call hipster_cond lezP leq proves lezP y ⟹ lezP x = leq x y but returns the (invalid) lemma

lemma ex01 [thy_expl]: "leq x3 y3 = True"
by (hipster_induct_simp_metis lezP.simps leq.simps)

See theory Examples/NatsBug.thy.