proposition: Lemma tiff_trans : forall a b c, (a <=> b) -> (b <=> c) -> (a <=> c).
proof: Proof. intros a b c i1 i2. destruct i1 as [i11 i12]. destruct i2 as [i21 i22]. split; intro k. apply i11 in k; apply i21 in k; auto. apply i22 in k; apply i12 in k; auto. Qed.
imports: universe