cicInspect: node count fixed

[helm.git] / helm / software / matita / contribs / character / classes / defs.ma

diff --git a/helm/software/matita/contribs/character/classes/defs.ma b/helm/software/matita/contribs/character/classes/defs.ma
index d5986fe7779a5d20926408cdc9cbef0c7e57a1ee..add242cc449f33d9655fb2b46bbb4e5a59eb318e 100644 (file)
--- a/helm/software/matita/contribs/character/classes/defs.ma
+++ b/helm/software/matita/contribs/character/classes/defs.ma
@@ -25,3 +25,8 @@ with T: nat \to Prop \def
    | t1: \forall i. P i \to T (i * 3)
    | t2: \forall i. T i \to T (i * 3)
 .
+
+inductive S: nat \to Prop \def
+   | s1: \forall i. P i \to S (i * 2)
+   | s2: \forall i. T i \to S (i * 2)
+.