test(tests/lean): add new normalizer/elaborator test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

tests/lean/norm_bug1.lean

@@ -0,0 +1,31 @@
+SetOption pp::colors false
+
+Definition TypeM := (Type M)
+Definition TypeU := (Type U)
+Variable CastEq {A : TypeU} {A' : TypeU} (H : A == A') (x : A) : x == cast H x
+
+Check fun (A A': TypeM)
+          (a   : A)
+          (b   : A')
+          (L2  : A' == A),
+   let b' : A        := cast   L2 b,
+       L3 : b == b'  := CastEq L2 b
+   in L3
+
+Check fun (A A': TypeM)
+          (B   : A -> TypeM)
+          (B'  : A' -> TypeM)
+          (f   : Pi x : A, B x)
+          (g   : Pi x : A', B' x)
+          (a   : A)
+          (b   : A')
+          (H1  : (Pi x : A, B x) == (Pi x : A', B' x))
+          (H2  : f == g)
+          (H3  : a == b),
+    let L1 : A  == A'               := DomInj H1,
+        L2 : A' == A                := Symm L1,
+        b' : A                      := cast L2 b,
+        L3 : b  == b'               := CastEq L2 b,
+        L4 : a == b'                := TransExt H3 L3,
+        L5 : f a == f b'            := Congr2 f L4
+    in L5

tests/lean/norm_bug1.lean.expected.out

@@ -0,0 +1,34 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Set: pp::colors
+  Defined: TypeM
+  Defined: TypeU
+  Assumed: CastEq
+λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := CastEq L2 b in L3 :
+    Π (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b
+λ (A A' : TypeM)
+  (B : A → TypeM)
+  (B' : A' → TypeM)
+  (f : Π x : A, B x)
+  (g : Π x : A', B' x)
+  (a : A)
+  (b : A')
+  (H1 : (Π x : A, B x) == (Π x : A', B' x))
+  (H2 : f == g)
+  (H3 : a == b),
+  let L1 : A == A' := DomInj H1,
+      L2 : A' == A := Symm L1,
+      b' : A := cast L2 b,
+      L3 : b == b' := CastEq L2 b,
+      L4 : a == b' := TransExt H3 L3,
+      L5 : f a == f b' := Congr2 f L4
+  in L5 :
+    Π (A A' : TypeM)
+      (B : A → TypeM)
+      (B' : A' → TypeM)
+      (f : Π x : A, B x)
+      (g : Π x : A', B' x)
+      (a : A)
+      (b : A')
+      (H1 : (Π x : A, B x) == (Π x : A', B' x)),
+      f == g → a == b → f a == f (Cast A' A (Symm (DomInj H1)) b)