telescopes.ref 431 Bytes
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
1 subgoal
  
  X : tele
  α, β, γ1, γ2 : X → Prop
  ============================
  accessor α β γ1 → accessor α β (λ.. x : X, γ1 x ∨ γ2 x)
1 subgoal
  
  X : tele
  α, β, γ1, γ2 : X → Prop
  ============================
  ∀.. x : X, γ1 x → (λ.. x0 : X, γ1 x0 ∨ γ2 x0) x
1 subgoal
  
  X : tele
  α, β, γ1, γ2 : X → Prop
  x : X
  Hγ : γ1 x
  ============================
  γ1 x ∨ γ2 x