case a.h
l : Type ?u.1214447
m : Type u_1
n : Type ?u.1214453
o : Type ?u.1214456
m' : o → Type ?u.1214461
n' : o → Type ?u.1214466
R : Type ?u.1214469
S : Type ?u.1214472
α : Type v
β : Type w
γ : Type ?u.1214479
inst✝ : Star α
v : m → α
i✝ : m
x✝ : Unit
⊢ (row v)ᴴ i✝ x✝ = col (star v) i✝ x✝
l : Type ?u.1214447
m : Type u_1
n : Type ?u.1214453
o : Type ?u.1214456
m' : o → Type ?u.1214461
n' : o → Type ?u.1214466
R : Type ?u.1214469
S : Type ?u.1214472
α : Type v
β : Type w
γ : Type ?u.1214479
inst✝ : Star α
v : m → α
⊢ (row v)ᴴ = col (star v)
ext
no goals
case a.h
l : Type ?u.1214447
m : Type u_1
n : Type ?u.1214453
o : Type ?u.1214456
m' : o → Type ?u.1214461
n' : o → Type ?u.1214466
R : Type ?u.1214469
S : Type ?u.1214472
α : Type v
β : Type w
γ : Type ?u.1214479
inst✝ : Star α
v : m → α
i✝ : m
x✝ : Unit
⊢ (row v)ᴴ i✝ x✝ = col (star v) i✝ x✝
rfl