case a.h
l : Type ?u.1213129
m : Type u_1
n : Type ?u.1213135
o : Type ?u.1213138
m' : o → Type ?u.1213143
n' : o → Type ?u.1213148
R : Type ?u.1213151
S : Type ?u.1213154
α : Type v
β : Type w
γ : Type ?u.1213161
inst✝ : Add α
v w : m → α
i✝ : Unit
x✝ : m
⊢ row (v + w) i✝ x✝ = (row v + row w) i✝ x✝
l : Type ?u.1213129
m : Type u_1
n : Type ?u.1213135
o : Type ?u.1213138
m' : o → Type ?u.1213143
n' : o → Type ?u.1213148
R : Type ?u.1213151
S : Type ?u.1213154
α : Type v
β : Type w
γ : Type ?u.1213161
inst✝ : Add α
v w : m → α
⊢ row (v + w) = row v + row w
ext
no goals
case a.h
l : Type ?u.1213129
m : Type u_1
n : Type ?u.1213135
o : Type ?u.1213138
m' : o → Type ?u.1213143
n' : o → Type ?u.1213148
R : Type ?u.1213151
S : Type ?u.1213154
α : Type v
β : Type w
γ : Type ?u.1213161
inst✝ : Add α
v w : m → α
i✝ : Unit
x✝ : m
⊢ row (v + w) i✝ x✝ = (row v + row w) i✝ x✝
rfl