∀ {prop proof : Lean.Expr} {generation : ℕ} {prop_1 proof_1 : Lean.Expr} {generation_1 : ℕ},
  Lean.Meta.Grind.NewFact.fact prop proof generation = Lean.Meta.Grind.NewFact.fact prop_1 proof_1 generation_1 →
    prop = prop_1 ∧ proof = proof_1 ∧ generation = generation_1