//
// Created by Dependently-Typed Lambda Calculus on 2019-12-04
// id-func
// Author: ice10
//

definition id : {A : Type} -> A -> A;
clause id a = a;

definition flip : {A : Type}
   -> (A -> A -> A) -> A -> A -> A;
clause flip f a b = f b a;

definition flip' : {A B C : Type}
   -> (A -> B -> C) -> B -> A -> C;
clause flip' f a b = f b a;

definition flip''' : {A : Type}
   -> (A -> A -> A) -> A -> A -> A;
clause flip''' f a b = flip f a b;

definition flip'' : {A : Type}
   -> (A -> A -> A) -> A -> A -> A;
clause flip'' f a b = flip' f a b;