∀ {fst snd : Lean.Expr.ProdTree} {lfst lsnd : Lean.Level} {fst_1 snd_1 : Lean.Expr.ProdTree}
  {lfst_1 lsnd_1 : Lean.Level},
  fst.prod snd lfst lsnd = fst_1.prod snd_1 lfst_1 lsnd_1 → fst = fst_1 ∧ snd = snd_1 ∧ lfst = lfst_1 ∧ lsnd = lsnd_1