File: bug_19557_2.v

package info (click to toggle)
coq 9.1.0%2Bdfsg-3
  • links: PTS, VCS
  • area: main
  • in suites: experimental
  • size: 35,964 kB
  • sloc: ml: 239,908; sh: 4,355; python: 2,985; ansic: 2,644; makefile: 874; lisp: 171; javascript: 63; xml: 24; sed: 2
file content (21 lines) | stat: -rw-r--r-- 382 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
 

Definition not (A : Type) := A -> False.

Record HProp := {
  hprop_type : Type ;
}.

Coercion hprop_type : HProp >-> Sortclass.

Definition merely (A : Type) : HProp.
Admitted.

Section SwapTypes.

  Context (A B : Type).

  Lemma foo X (p:merely (X = B)) :
    sigT (fun p0 : not (merely (X = A)) => merely (X = B)).
    refine (existT _ (fun q => _) p).
  Abort.
End SwapTypes.