From 45c95bf073c4f4b422fbf9ca9497d03a17e3746e Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 10 Feb 2011 12:19:56 +0000
Subject: [PATCH] Added typing rule for dummies

---
 matita/matita/lib/lambda/types.ma | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/matita/matita/lib/lambda/types.ma b/matita/matita/lib/lambda/types.ma
index 09ecd4e05..2a89549d6 100644
--- a/matita/matita/lib/lambda/types.ma
+++ b/matita/matita/lib/lambda/types.ma
@@ -49,7 +49,9 @@ inductive TJ: list T → T → T → Prop ≝
   | abs: ∀G.∀A,B,b.∀i. 
      TJ (A::G) b B → TJ G (Prod A B) (Sort i) → TJ G (Lambda A b) (Prod A B)
   | conv: ∀G.∀A,B,C.∀i. conv B C →
-     TJ G A B → TJ G B (Sort i) → TJ G A C.
+     TJ G A B → TJ G B (Sort i) → TJ G A C
+  | dummy: ∀G.∀A,B.∀i. 
+     TJ G A B → TJ G B (Sort i) → TJ G (D A) B.
      
 notation "hvbox(G break  ⊢ A : B)" non associative with precedence 50 for @{'TJ $G $A $B}.
 interpretation "type judgement" 'TJ G A B = (TJ G A B).
@@ -204,9 +206,10 @@ theorem substitution_tj:
       [#H (normalize in H) (applyS H) | normalize // ]
     ]
   |#G #P #Q #R #i #convQR #tjP #tjQ #Hind1 #Hind2
-   #G1 #D #N #Heq #tjN (normalize in Hind1 ⊢ %)
-   @(conv …(conv_subst … convQR) ? (Hind2 …)) //
-   @Hind1 //
+   #G1 #D #N #Heq #tjN
+   @(conv …(conv_subst … convQR) ? (Hind2 …)) // @Hind1 //
+  |#G #P #Q #i #tjP #tjQ #Hind1 #Hind2
+   #G1 #D #N #Heq #tjN @dummy /2/ 
   ]
 qed.
  
-- 
2.39.2