1 2 3 4 5 6
1 goal X : tele α, β, γ1, γ2 : X → Prop ============================ accessor α β γ1 → accessor α β (λ.. x : X, γ1 x ∨ γ2 x)