File "./output/unification.v", line 9, characters 35-39:
The command has indeed failed with message:
In environment
x : T
T : Type
a : T
Unable to unify "T" with "?X@{x0:=x; x:=C a}" (cannot instantiate
"?X" because "T" is not in its scope: available arguments are
"x" "C a").
File "./output/unification.v", line 12, characters 12-14:
The command has indeed failed with message:
The term "id" has type "ID" while it is expected to have type
"Type -> ?T" (cannot instantiate "?T" because "A" is not in its scope).
1 focused goal (shelved: 1)
H : forall x : nat, S (S (S x)) = x
============================
?x = 0
1 focused goal (shelved: 1)
H : forall x : nat, S (S (S x)) = x
============================
?x = 0
1 focused goal (shelved: 1)
H : forall x : nat, S (S (S x)) = x
============================
?x = 0
1 focused goal (shelved: 1)
H : forall x : nat, S x = x
============================
?y = 0
1 focused goal (shelved: 3)
T : Prop
H : forall Q R S : Prop, (Q /\ R) /\ S -> T
============================
(?Q /\ ?R) /\ ?S
[ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
]
