Thanks for this wonderful library! I have played with it a bit, trying to apply to some simple but more realistic problems. What I found most frustrating is that I cannot figure out how to derive new proof with existing ones.

Take the less_than_eq proof as an example:

pub mod less_than_eq
{
  use mononym::*;

  proof! {
    LessThanEq(x: u32, y: u32);
  }

  pub fn check_less_than_eq<XVal: HasType<u32>, YVal: HasType<u32>>(
    x: &Named<XVal, u32>,
    y: &Named<YVal, u32>,
  ) -> Option<LessThanEq<XVal, YVal>>
  {
    if x.value() <= y.value() {
      Some(LessThanEq::new())
    } else {
      None
    }
  }
}

And I want to add a simple function:

pub fn at_most(x: u32, y: u32) -> u32 {
    if x <= y {
        x
    } else {
        y
    }
}

Ideally, I could write this function (with a LessThanEq<ZVal, YVal> proof) outside the less_than_eq module. However, what I finally struggled to achieve was something like this, inside less_than_eq module:

pub struct ExistLessThanEq<
    ZVal: HasType<u32>,
    YVal: HasType<u32>,
> {
    pub z: Named<ZVal, u32>,
    pub y: Named<YVal, u32>,
    pub less_than_eq: LessThanEq<ZVal, YVal>,
}

pub fn at_most(x: u32, y: u32, seed: Seed<impl Name>)
    -> ExistLessThanEq<impl HasType<u32>, impl HasType<u32>>
{
    let (seed1, seed2) = seed.replicate();
    if x <= y {
        ExistLessThanEq {
            z: seed1.new_named(x),
            y: seed2.new_named(y),
            less_than_eq: LessThanEq::new(),
        }
    } else {
        ExistLessThanEq {
            z: seed1.new_named(y),
            y: seed2.new_named(y),
            less_than_eq: LessThanEq::new(),
        }
    }
}

Note that I have to repeat x <= y comparison here.

I'm not quite familiar with dependently typed programing, but I believe there should be something better. Do you have any suggestions?