File: telescopes.ref

package info (click to toggle)
coq-stdpp 1.11.0-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 1,696 kB
  • sloc: makefile: 52; sh: 35; sed: 1
file content (22 lines) | stat: -rw-r--r-- 458 bytes parent folder | download | duplicates (2) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
 
1 goal
  
  X : tele
  α, β, γ1, γ2 : X → Prop
  ============================
  accessor α β γ1 → accessor α β (λ.. x : X, γ1 x ∨ γ2 x)
1 goal
  
  X : tele
  α, β, γ1, γ2 : X → Prop
  ============================
  ∀.. x : X, γ1 x → (λ.. x0 : X, γ1 x0 ∨ γ2 x0) x
1 goal
  
  X : tele
  α, β, γ1, γ2 : X → Prop
  x : X
  Hγ : γ1 x
  ============================
  γ1 x ∨ γ2 x
[TEST x y : nat, x = y]
     : Prop