module exampleLetExpressionRecord where

postulate A : Set
postulate B : Set
postulate C : Set
postulate D : Set

record AB : Set where
 field 
    a : A
    b : B

record CD : Set where
 field
   c : C
   d : D

f : (A -> C) -> (B -> D) -> AB -> CD
f a-c b-d ab   = let a' : A 
                     a' = AB.a ab
                     b' : B 
                     b' = AB.b ab
                     c : C 
                     c = a-c a'
                     d : D  
                     d = b-d b'
                 in  record{c = c;d = d}