conversion fails to reduce enough in the presence of sprop

[JasonGross]

Description of the problem

I am not sure if this is a bug with rocq-lean-import or with Rocq, cf rocq-community/rocq-lean-import#45 (comment)

pnni.txt

Small Rocq / Coq file to reproduce the bug

From LeanImport Require Import Lean.
Lean Import "pnni.txt" 1 67843.
Goal forall n' m',
@eq Bool
    (Lean_Omega_Constraint_sat'
       (Lean_Omega_tidyConstraint
          (Lean_Omega_Constraint_mk
             (Option_some_inst1 Int
                (OfNat_ofNat_inst1 Int Nat_zero (instOfNat Nat_zero)))
             (Option_some_inst1 Int
                (OfNat_ofNat_inst1 Int Nat_zero (instOfNat Nat_zero))))
          (List_cons_inst1 Int
             (OfNat_ofNat_inst1 Int (Nat_succ (Nat_succ Nat_zero))
                (instOfNat (Nat_succ (Nat_succ Nat_zero))))
             (List_cons_inst1 Int
                (Neg_neg_inst1 Int Int_instNegInt
                   (OfNat_ofNat_inst1 Int (Nat_succ (Nat_succ Nat_zero))
                      (instOfNat (Nat_succ (Nat_succ Nat_zero)))))
                (List_nil_inst1 Int))))
       (Lean_Omega_tidyCoeffs
          (Lean_Omega_Constraint_mk
             (Option_some_inst1 Int
                (OfNat_ofNat_inst1 Int Nat_zero (instOfNat Nat_zero)))
             (Option_some_inst1 Int
                (OfNat_ofNat_inst1 Int Nat_zero (instOfNat Nat_zero))))
          (List_cons_inst1 Int
             (OfNat_ofNat_inst1 Int (Nat_succ (Nat_succ Nat_zero))
                (instOfNat (Nat_succ (Nat_succ Nat_zero))))
             (List_cons_inst1 Int
                (Neg_neg_inst1 Int Int_instNegInt
                   (OfNat_ofNat_inst1 Int (Nat_succ (Nat_succ Nat_zero))
                      (instOfNat (Nat_succ (Nat_succ Nat_zero)))))
                (List_nil_inst1 Int))))
       (Lean_Omega_Coeffs_ofList
          (List_cons_inst1 Int (Nat_cast_inst1 Int instNatCastInt n')
             (List_cons_inst1 Int (Nat_cast_inst1 Int instNatCastInt m')
                (List_nil_inst1 Int)))))
    Bool_true ->
 @eq Bool
    (Lean_Omega_Constraint_sat'
       (Lean_Omega_Constraint_mk
          (Option_some_inst1 Int
             (OfNat_ofNat_inst1 Int Nat_zero (instOfNat Nat_zero)))
          (Option_some_inst1 Int
             (OfNat_ofNat_inst1 Int Nat_zero (instOfNat Nat_zero))))
       (List_cons_inst1 Int
          (OfNat_ofNat_inst1 Int (Nat_succ Nat_zero)
             (instOfNat (Nat_succ Nat_zero)))
          (List_cons_inst1 Int
             (Neg_neg_inst1 Int Int_instNegInt
                (OfNat_ofNat_inst1 Int (Nat_succ Nat_zero)
                   (instOfNat (Nat_succ Nat_zero))))
             (List_nil_inst1 Int)))
       (Lean_Omega_Coeffs_ofList
          (List_cons_inst1 Int (Nat_cast_inst1 Int instNatCastInt n')
             (List_cons_inst1 Int (Nat_cast_inst1 Int instNatCastInt m')
                (List_nil_inst1 Int)))))
    Bool_true.
    intros n' m'.
    Fail intro x; exact x. (* type mismatch *)
    cbv. (* Alt: cbn. cbv [Lean_Omega_Constraint_div]. *)
    intro x; exact x. (* success *)
Fail Qed.

Version of Rocq / Coq where this bug occurs

db6bc65

Interface of Rocq / Coq where this bug occurs

No response

Last version of Rocq / Coq where the bug did not occur

No response