Description of the problem

Trying to capture an Int63 number X in a proof using a pattern fails with Error: term X does not match any subterm in the goal.

Example:

Require Import Int63 ssreflect ssrfun ssrbool.

Lemma test : 43%int63 = (42 + 1)%int63.
Proof. set X := 43%int63. (* does not capture int63 *)

Coq Version

Coq 8.11.2

There is now a type circle in UniMath.SyntheticHomotopyTheory.Circle2. It would be great to define pi_1 of a pointed type, and to show that pi_1(circle, pt) \simeq Z.