Function lemma_incl_transitive Copy item path

pub proof fn lemma_incl_transitive<RA: ResourceAlgebra>(a: RA, b: RA, c: RA)

incl(a, b),

incl(b, c),

incl(a, c),