name: "dep";
version: "0.1.0";
description: "add your description here";
functions {
  dep_tup_intro : ((a : x)^true & (b : p(a))^true) -> ((a, b) : (a : x, p(a)))^true;
  dep_tup_ty : ((a : x) & (b : y)^a) -> ((a, b) : (x, y));
  dep_tup_ty_formation : ((x : type'(z'))^true & (p(a) : type'(z'))^(a : x)) -> ((a : x, p(a)) : type'(z'))^true;
}
dependencies {
}