-lemma eq_false_inv_beta: ∀V1,V2,W1,W2,T1,T2.
- (ⓐV1. ⓛW1. T1 = ⓐV2. ⓛW2 .T2 →False) →
- (W1 = W2 → False) ∨
- (W1 = W2 ∧ (ⓓV1. T1 = ⓓV2. T2 → False)).
-#V1 #V2 #W1 #W2 #T1 #T2 #H
+lemma eq_false_inv_beta: ∀a,V1,V2,W1,W2,T1,T2.
+ (ⓐV1. ⓛ{a}W1. T1 = ⓐV2. ⓛ{a}W2 .T2 → ⊥) →
+ (W1 = W2 → ⊥) ∨
+ (W1 = W2 ∧ (ⓓ{a}V1. T1 = ⓓ{a}V2. T2 → ⊥)).
+#a #V1 #V2 #W1 #W2 #T1 #T2 #H