CyberShadow

#!/bin/env rdmd
module xorg_show_grabs;

import std.algorithm;
import std.conv;
import std.exception;
import std.getopt;
import std.stdio;
import std.string;

gallais

Require Import Coq.Setoids.Setoid.
Require Import Arith.

Notation "`Begin p" := p (at level 20, right associativity).
Notation "a =] p ] pr" := (@eq_trans _ a _ _ p pr) (at level 30, right associativity).
Notation "a =[ p [ pr" := (@eq_trans _ a _ _ (eq_sym p) pr) (at level 30, right associativity).
Notation "a `End" := (@eq_refl _ a) (at level 10).

Definition times2 : forall n, n + n = 2 * n := fun n =>
  `Begin