Dummy dependent types are no longer cleaned in inductive type arities.

[helm.git] / helm / software / matita / library / algebra / CoRN / SemiGroups.ma

diff --git a/helm/software/matita/library/algebra/CoRN/SemiGroups.ma b/helm/software/matita/library/algebra/CoRN/SemiGroups.ma
index b57d3b2fde5f22d2a735e277df8be2f35090d085..8613d83e2ba486c110c817fed6107ef41c33179b 100644 (file)
--- a/helm/software/matita/library/algebra/CoRN/SemiGroups.ma
+++ b/helm/software/matita/library/algebra/CoRN/SemiGroups.ma
@@ -187,8 +187,8 @@ lemma part_function_plus_strext :  \forall G:CSemiGroup. \forall F,F': PartFunct
   \to x \neq y.
 intros (G F F' x y Hx Hy H).
 elim (bin_op_strext_unfolded ? ? ? ? ? ? H)[
-apply pfstrx[apply F|elim Hx.apply t|elim Hy.apply t|exact H1]|
-apply pfstrx[apply F'|elim Hx.apply t1|elim Hy.apply t1|exact H1]]
+apply pfstrx[apply F|elim Hx.apply a|elim Hy.apply a|exact H1]|
+apply pfstrx[apply F'|elim Hx.apply b|elim Hy.apply b|exact H1]]
 qed.
 
 definition Fplus : \forall G:CSemiGroup. \forall F,F': PartFunct G. ? \def