proposition: Lemma case_L_R (P : forall n m, t (n + m) -> Type) {n m} (p : t (n + m)) : (forall n m (q : t n), P n m (L m q)) -> (forall n m (q : t m), P n m (R n q)) -> P n m p.
proof: Proof. intros HL HR. apply case_L_R'; intros q. - apply HL. - apply HR. Qed.
imports: PeanoNat