proposition: Lemma fin_add_inv_l {n1 n2} (P : fin (n1 + n2) → Type) (H1: ∀ i1 : fin n1, P (Fin.L _ i1)) (H2: ∀ i2, P (Fin.R _ i2)) (i: fin n1) : fin_add_inv P H1 H2 (Fin.L n2 i) = H1 i.
proof: Proof. revert P H1 H2 i. induction n1 as [|n1 IH]; intros P H1 H2 i; inv_fin i; simpl; auto. intros i. apply (IH (λ i, P (FS i))). Qed.
imports: stdpp(options)