//
// Created by Dependently-Typed Lambda Calculus on 2019-06-16
// id-flip
// Author: ice1000
//

val id: {A : Type} -> A -> A;
let id = \a. a;

val flip : {A B C : Type}
         -> (A -> B -> C)
         -> (B -> A -> C);
let flip = \f a b. id (f b a);

let idId = (^id) id;