2010-04-21から1日間の記事一覧
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). %termina…