Ajout de la β-réduction du λ-terme final.
This commit is contained in:
@@ -0,0 +1,10 @@
|
||||
(A -> B -> C) -> (B -> A -> C)
|
||||
intro f.
|
||||
intro b.
|
||||
intro a.
|
||||
cut (B -> C).
|
||||
intro bc.
|
||||
apply bc.
|
||||
assumption.
|
||||
apply f.
|
||||
assumption.
|
||||
Reference in New Issue
Block a user