Browse Source

Make example even more complex

hydraz 2 years ago
parent
commit
ccced2c25d
1 changed files with 3 additions and 2 deletions
  1. 3 2
      example.dtt

+ 3 - 2
example.dtt

@@ -26,6 +26,7 @@ define Transitive := /\α.
                        (pb: Eq α b c). Refl α a.
 
 let pair = MkPair Nat Nat Z (S Z);
-  case pair of {
+let tp = case pair of {
     (MkPair α β a b) -> Eq β b b
-  }
+  };
+  (Refl Nat (S Z) : tp)