ind c ⟦a⟧ : B ⟦a⟧
c a : B ⟦a⟧
c a