aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/bug_9403.out
blob: 850760d5ede8c22b67d973a62a2666e718ce4750 (plain)
1
2
3
4
5
6
1 subgoal
  
  X : tele
  α, β, γ1, γ2 : X → Prop
  ============================
  accessor α β γ1 → accessor α β (λ.. x : X, γ1 x ∨ γ2 x)