この一週間くらい手を動かしてた、Software Foundationsの「サブシーケンスという関係は推移的である。」ということの証明が出来た!めっさうれしい。 Inductive subseq : list nat -> list nat -> Prop := | subseq_nil : subseq [] [] | subseq_e : forall …
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。