Function subst_app 

pub fn subst_app<F: Prop, A: Prop, B: Prop, C: Prop>() -> Eq<Subst<App<F, A>, B, C>, App<Subst<F, B, C>, Subst<A, B, C>>>

f(a)[b := c] == f[b := c](a[b := c]).