no goals
L : Language
L' : Language
c f₁ f₂ : Type u
r₁ r₂ : Type v
⊢ card (Language.mk₂ c f₁ f₂ r₁ r₂) = lift (#c) + lift (#f₁) + lift (#f₂) + lift (#r₁) + lift (#r₂)
simp [card_eq_card_functions_add_card_relations, add_assoc]