proposition: Lemma Is_true_irrel (b : bool) (p q : b) : p = q.
proof: Proof. destruct b. destruct p, q. reflexivity. destruct p. Defined.
imports: Program.Basics Program.Tactics Equations(Equations) ZArith Lia Psatz Nat Coq.Vectors.VectorDef