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