Function subst_const 

pub fn subst_const<A: Prop, B: Prop, C: Prop>(
    _a_is_const: IsConst<A>,
) -> Eq<Subst<A, B, C>, A>

is_const(a) => (a[b := c] == a).