Commit 598ae8bc authored by MARCHE Claude's avatar MARCHE Claude

bug 13849

parent 55889253
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Inductive t :=
| T : t .
Inductive x (a:Type) (b:Type) :=
| X : t -> a -> x a b
| Y : t -> b -> x a b.
Set Contextual Implicit.
Implicit Arguments X.
Unset Contextual Implicit.
Set Contextual Implicit.
Implicit Arguments Y.
Unset Contextual Implicit.
Inductive a :=
| A0 : a
| A1 : a .
Inductive b :=
| B : b .
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem x1 : ((X(T, A0):(x a b)) = (X(T, A1):(x a b))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -5,7 +5,7 @@
<prover
id="0"
name="Coq"
version="8.3pl3"/>
version="8.2pl2"/>
<file
name="../13849.why"
verified="false"
......@@ -26,7 +26,7 @@
shape="ainfix =ab1ab2">
<proof
prover="0"
timelimit="5"
timelimit="10"
edited="13849_T_x_1.v"
obsolete="true"
archived="false"><unedited/>
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment