ranha https://blog.hatena.ne.jp/ranha/ Yet Another Ranha https://ranha.hatenadiary.org/ tm : type. step : tm -> tm -> type. sn : tm -> type. sn_ : ({U:tm} step T U -> sn U) -> sn T. lem : (sn T) -> (step T U) -> (sn U) -> type. %mode lem +D1 +D2 -D3. lem_pr : lem (sn_ Pred : sn T) (StepTU : step T U) (Pred U StepTU). %terminates {} (lem _ _ _).まずそもそもの所、これで上手くやりたい事が出来ているのかどうか分からないのですが・・… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Franha.hatenadiary.org%2Fentry%2F20100421%2F1271779031" title="fresh vs forall - Yet Another Ranha" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2010-04-21 00:57:11 rich https://ranha.hatenadiary.org/entry/20100421/1271779031 1.0 100%