combine_splitが分からん。 証明は出来た。しかしどやってdestructを使うのか分からねえ。 Theorem split_fst_snd : forall (X Y: Type) ( l : list (X * Y)), split l = ((fst (split l)), (snd (split l))). Proof. intros. induction l as [| [x y] l']. …
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。