feat: ignore explicit proofs in canonicalizer

src/Lean/Meta/Canonicalizer.lean

@@ -101,7 +101,7 @@ private partial def mkKey (e : Expr) : CanonM Key := do
         let args ← e.getAppArgs.mapIdxM fun i arg => do
           if h : i < info.paramInfo.size then
             let info := info.paramInfo[i]
-            if info.isExplicit then
+            if info.isExplicit && !info.isProp then
               pure (← mkKey arg).e
             else
               pure (mkSort 0) -- some dummy value for erasing implicit

tests/lean/run/omegaCanon.lean

@@ -7,7 +7,7 @@ def filter (p : α → Prop) [inst : DecidablePred p] (xs : List α) : List α :
       -- but definitionally equal.
       x :: @filter α p (fun x => inst x) xs'
     else
-      filter p xs'
+      @filter α p inst xs'
 
 def filter_length (p : α → Prop) [DecidablePred p] : (filter p xs).length ≤ xs.length := by
   induction xs with
@@ -15,3 +15,25 @@ def filter_length (p : α → Prop) [DecidablePred p] : (filter p xs).length ≤
   | cons x xs ih =>
     simp only [filter]
     split <;> simp only [List.length] <;> omega
+
+inductive Op where
+  | bla
+  | foo (a : Nat)
+
+def Op.ctorIdx : Op → Nat
+  | .bla => 0
+  | .foo .. => 1
+
+def Op.fooData (o : Op) (h : o.ctorIdx = 1) : Nat :=
+  match o, h with
+  | .foo a, _ => a
+
+theorem ex (o₁ o₂ o₃ : Op)
+    (h₁ : o₁.ctorIdx = 1)
+    (h₂ : o₁.ctorIdx = o₂.ctorIdx)
+    (h₃ : o₂.ctorIdx = o₃.ctorIdx)
+    (h₄ : o₂.ctorIdx = 1)
+    (_ : o₁.fooData h₁ < o₂.fooData h₄)
+    (_ : o₂.fooData (h₂ ▸ h₁) < o₃.fooData (h₃ ▸ h₄))
+    : o₁.fooData h₁ < o₃.fooData (h₃ ▸ h₄) := by
+  omega