
  0 | module Proofs.Congruence
  1 | 
  2 | public export
  3 | cong2Dep :
  4 |   {0 t1 : Type} ->
  5 |   {0 t2 : t1 -> Type} ->
  6 |   (f : ((x : t1) -> t2 x -> t3)) ->
  7 |   {0 a, b : t1} ->
  8 |   {0 c : t2 a} ->
  9 |   {0 d : t2 b} ->
 10 |   (p : a === b) ->
 11 |   c === (rewrite p in d) ->
 12 |   f a c = f b d
 13 | cong2Dep f Refl Refl = Refl
 14 | 
 15 | public export
 16 | app : (f : a -> b) -> (g : a -> b) -> f === g -> (x : a) -> f x === g x
 17 | app f f Refl x = Refl
 18 | 
 19 |